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.
* 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.
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.
* Added single step meta-function to core
* Expose step/syn in redex-lang
* Added macro to sugar for convenience use
* Updated relevant docs (also fixed bug in reflection docs)
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.
* run is user-definable through the existing reflection features; moved
to sugar.
* define need not have special function support in curnel; moved to
sugar.
* fixed relevant documentation
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.
* Various style fixes
* Standardize the proof state interface/naming a little.
* Reorganized base.rkt; now easier to read
* Fixed some mismatch code/documentation
* Renamed "basic" to "standard"; basic was too close to base, and not
really helpful.
* Added the Sartactics library, provides a sassy wrapper around the basic
tactics.
* Added prefix-in, although it probably only works for macros
* Better syntax for define-tactic
