Cur can now type check elim without a discriminant. Unfortunately, this
breaks the API of elim. Fortunately, the typing rule for elim is easier
to understand, and it is easier to partially apply elim.
These fixes are merged because properly testing the latter requires
having the former, while properly implementing the former is made
simpler by having the latter.
Fixed handling of names/substitution
===
* Added capture-avoiding substitution. Closes#7
* Added equivalence during typing checking, including α-equivalence and
limited β-equivalence. Closes#8
* Exposed better typing-check reflection features to allow typing
checking modulo equivalence.
* Tweaked QED macro to use new type-checking reflection feature.
Fixed inductive families
===
The implementation of inductive families is now based on the theoretical
models of inductive families, rather than an ad-hoc non-dependent
pattern matcher.
* Removed case and fix from Cur and Curnel. They are replaced by elim,
the generic eliminator for inductive families. Closes#5. Since fix is
no more, also closes#2.
* Elimination of false works! Closes#4.
* Changed uses of case to elim in Curnel
* Changed uses of case* in Cur to use eliminators. Breaks case* API.
* Fixed Coq generator to use eliminators
* Fixed Latex generator
* Type should be not be in the core language. Converted all uses of Type
to Unv 0, potentially fixing a universe bug in the process.
* Added macro Type to Curnel that enables existing code to work more or
less as before.
* Split prop, nat, bool, maybe, and stlc into modules
* Reverted proofs-for-free stuff to the pre-me-fucking-about version,
and cleaned it up.
* Fixed redex-curnel test suite. Redefinition of module+ was causing
issues.
* Moved various var stuff to oll.
* Moved stlc examples to seperate module.
* Removed auto currying from core. These are now provided by sugar.
* Exposed type-infer, type-check, and normalize
* Attempting to track down strange bugs regarding local-expand
* sigma, gamma extended at expand time
* All type-checking happens at expand time
* Locally expand all forms into core redex forms. However, this seems to
be causing problems. Probably not controlling expansion just right.
