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, philngu...@gmail.com 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 beatriz....@gmail.com > 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 racket-users+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/684893ee-9383-43bf-848a-dd217eb0b405n%40googlegroups.com.
