These macros were not really serving a good purpose. They were defined
early on to demonstrate that metaprogramming can give us Coq-like
notation, but really, we have much more interesting demos.
Replaces all identifiers with their definitions before type-checking.
Enables more type-checking, but *realllly* slows down type-checking.
Also a test case.
Fixed eliminator reduction for eliminators of inductive types whose
constructors do not have the same parameters as their type. The
canonical example is ==, which has 3 parameters, but whose constructor
refl only has two.
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
