William J. Bowman
|
176f08dd92
|
Added inductive types; assorted fixes
* Fixed variable typing; weakening is no longer a rule but built into
lookup logic.
* Fixed substitution.
|
2014-07-16 18:51:02 +02:00 |
|
William J. Bowman
|
944e9690dc
|
Fixed rule names, working on type inference
|
2014-07-12 23:46:02 +02:00 |
|
William J. Bowman
|
0b004d9ccb
|
Added type reduction and infer-core
* Can't get β-equiv rule to work, so normalize types then check.
* Added infer-core, a closer to surface language on which to do
inference.
|
2014-07-12 22:28:57 +02:00 |
|
William J. Bowman
|
7179e30fe1
|
Removed annotation from core language
|
2014-07-12 22:28:06 +02:00 |
|
William J. Bowman
|
4b1735d435
|
First draft of redex core language.
|
2014-07-12 21:00:04 +02:00 |
|