* Made the primitive form of elim (elim t_0 t_1), allowing this form to be
considered a value when t_0 and t_1 are values.
* Moved definition of values to reduction language, and fixed it. This
fixed issues with unique decomposition, and thus fixed reduction of
eliminators.
* Enabled caching in apply-reduction-relation* to speed up results of
recursive calls.
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.
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
