William J. Bowman
b57f2d4a85
STLC now works! Or, type-checks.
2015-01-20 00:56:18 -05:00
William J. Bowman
124531e3c2
Added TODOs of various new features
...
* Added description of new reflection features
* Cleaned up assorted comments
2015-01-20 00:55:37 -05:00
William J. Bowman
aaec536cf5
Fixed bad calls to terminates?
2015-01-20 00:55:23 -05:00
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
862d530b42
Added TODO about define/environments
2015-01-19 20:30:22 -05:00
William J. Bowman
de202fa6a0
Added plus, fixed some comments
2015-01-19 20:20:25 -05:00
William J. Bowman
c359631268
Added fix, without termination checking
...
Can now write recursive functions. Fix will probably change as I add
termination checking.
2015-01-19 20:15:55 -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
a5358575f3
Fixed to well-formed env, tinkering with PFF
2014-08-01 16:54:37 +02:00
William J. Bowman
ff4bd337fb
Added implementation of proofs for free extension
...
* Implemented the dual-mode extension to proofs for free, complete with
a neat theorem.
2014-07-28 18:25:42 +02:00
William J. Bowman
58619df30b
Serious reorganization of examples file
2014-07-28 18:25:28 +02:00
William J. Bowman
2c6daa6224
Fixed missing universe rule
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
febe276569
Renamed to racket-cic; language are cic*
2014-07-22 21:25:55 +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
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
