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.
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
* 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.
* 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.
