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.
