Thank you, I did just that! :D 4. Checking for membership in an environment sounds like a (very) decidable problem. It maybe simpler to just write a judgment form for the positive case, and simply defining the negative case as “when the judgment doesn’t hold”.
A sexta-feira, 9 de abril de 2021 à(s) 01:20:32 UTC+1, [email protected] escreveu: > It’s difficult without seeing the definitions, but here are a few general > comments: > > 1. Cases in judgment forms are not run in order. If multiple cases match, > they’ll all hold. For example, in this case, if (anotin ((a -> b ...)) a > #t) holds, (anotin ((a_0 -> b ...)) a #f) will also hold. > > 2. If your environment looks something like ((a_1 -> b_1) (a_2 -> b_2) > (a_3 -> b_3)), the pattern for the second case should be (_ ... (a -> b) > _ ...). The ellipses after b as it currently is means a sequence of zero > or more b’s. > > 3. The relation is being named “not in”, but it seems like it’s computing > both “in” and “not in” cases, which is confusing. > > 4. Checking for membership in an environment sounds like a (very) > decidable problem. It maybe simpler to just write a judgment form for the > positive case, and simply defining the negative case as “when the judgment > doesn’t hold”. > > On Wednesday, April 7, 2021 at 9:57:15 AM UTC-7 [email protected] > wrote: > >> Hello, >> I'm trying to write a side condition to a function, where it checks if a >> is in an environment ß. I tried this judgement by adding (judgment-holds >> (anotin (ß-v ...) a #f)) at the end of the function but it is not >> working :( >> Thank you! >> --Beatriz >> >> (define-judgment-form Flint >> #:mode (anotin I I O) >> #:contract (anotin env-ß a boolean) >> [------------------------- >> (anotin () a #f)] >> [------------------------- >> (anotin ((a -> b ...)) a #t)] >> [------------------------- >> (anotin ((a_0 -> b ...)) a #f)] >> [------------------------- >> (anotin (ß-v_0 ... (a -> b ...)) a #t)] >> [(anotin (ß-v ...) a boolean) >> ------------------------- >> (anotin (ß-v ... (a_0 -> b ...) ) a boolean)] >> ) >> > -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/684893ee-9383-43bf-848a-dd217eb0b405n%40googlegroups.com.
