William J. Bowman
f94894aacf
Draft of STLC with type system
...
* STLC + syntax for writing STLC terms naturally, without explicitly
applying inductive constructors.
* Complete STLC type system, although it's not quite correct yet.
2015-01-19 20:45:18 -05:00
William J. Bowman
de202fa6a0
Added plus, fixed some comments
2015-01-19 20:20:25 -05:00
William J. Bowman
ec38e652a7
Started modeling STLC
2015-01-19 13:15:16 -05:00
William J. Bowman
48360533b1
Added better case syntax, better thm/qed macros
2015-01-16 23:24:56 -05:00
William J. Bowman
89c5c1ba68
Fixed various bugs related to case and inductives
...
case would fail when used on an inductive family. Fixed this, added more
test cases, and cleaned up examples.
2015-01-16 22:54:35 -05:00
William J. Bowman
58619df30b
Serious reorganization of examples file
2014-07-28 18:25:28 +02:00
William J. Bowman
5d2988adf0
Extensive examples, syntax extensions out of core
2014-07-25 13:53:14 +02:00
William J. Bowman
754a32a3ea
Module language, positivity checking, more tests
...
* redex-core is now a module language, complete with fancyness. For
documentation, TODO.
* Added examples file using the module language.
2014-07-22 21:20:35 +02:00
