Added match, a better pattern matching construct than case.
Automatically infers inductive arguments, and feature a "recur" syntax.
Converted several functions from stdlib/nat to use this.
In dependent type system, Σ is normally the symbol for strong sums, not
signatures/declarations.
While Δ is sometimes used as an alternative to Γ, using it for
inductive signatures.
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.
* Renamed languages and reorganized languages
* Various fixes to fresh name generating
* Fixed to testing infrastructure; now tests modulo equivelance
* Renamed and reorganized many metafunctions, particularly those to do
with Σ and Γ
* Reorganized sections of code to improve readability and reduce
dependencies
* Reimplemented eliminator typing and reduction
* Various stylistic changes
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)
Previously, reflection procedures did not properly reify/reflect syntax
after evaluating in Redex. This limited compositionality of reflection
features.
No longer. Now all reflection procedures should reify their results back
into Cur syntax, and only top-level evaluation should result in Redex
datums (or explicit calls to cur->datum).
