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.
What is the purpose of giving all those rules? Would anyone actually use them instead of just using the definition? It seems to make it look unnecessarily complicated.
clarified that these rules are needed in some versions of predicative mathematics where one doesn’t have general function types and dependent function types
Anonymous
1 to 4 of 4