elim was not checking that the arguments to be used for the parameters
of the inductive matched the actual parameters expected, resulting in
incorrect and non-deterministic unification, and thus incorrect
reduction when the parameters were unified incorrectly.
Yesterday's changes to sugar broke some things:
* case isn't smart enough to infer the right things in all cases yet, so
added previously existing case* for when it is necessary.
* reexport define-theorem and qed from sugar, since still used in prop.
Moved all curnel code into curnel/, and split the two kernel modules
into separate files. Now the trusted core and the module/#lang stuff are
in separate files. The #lang is now reprovided by "cur.rkt", which
should also provide core agnostic sugar.
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
