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
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
2 matches
Mail list logo
