Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Looking at the section on “Guarded quantification” (here), I find the language a little odd, in how it keeps referring to “types” but really speaks very much as of sets.
I have adjusted wording slightly, but there remains room to improve the wording here, I think.
Also, I touched the typesetting of the two formulas, in order to make the form of the syntax tree visually more manifest.
1 to 2 of 2