William J. Bowman
e1ceb8a7d8
Renamed more curnels
2015-01-29 22:46:53 -05:00
William J. Bowman
c537287df4
Merge branch 'master' into reflection
2015-01-29 22:44:55 -05:00
William J. Bowman
ec95026066
Renamed kernel to curnel. An important pun.
2015-01-29 22:44:30 -05:00
William J. Bowman
8349ed1184
Shrinking core, added reflection tools
...
* Removed auto currying from core. These are now provided by sugar.
* Exposed type-infer, type-check, and normalize
* Attempting to track down strange bugs regarding local-expand
2015-01-28 15:27:20 -05:00
William J. Bowman
c24650ef01
Started work to enable reflection
...
* sigma, gamma extended at expand time
* All type-checking happens at expand time
* Locally expand all forms into core redex forms. However, this seems to
be causing problems. Probably not controlling expansion just right.
2015-01-27 23:55:50 -05:00
William J. Bowman
9ebc1723c6
Renamed project to cur. tehe
2015-01-27 19:07:17 -05:00
William J. Bowman
d508d9bcff
Started factoring into libraries.
2015-01-22 12:37:48 -05:00
William J. Bowman
f4a47cc7d6
Added coq code generator
2015-01-21 18:34:09 -05:00
William J. Bowman
6a29a1e4ef
stlc type system in new syntax, fixed import
...
* Finished the STLC type system in the new syntax!
* Fixed import/export of syntax/parse in redex-core
2015-01-21 09:55:43 -05:00
William J. Bowman
94926a42ee
Export all syntax-parse
2015-01-21 01:38:41 -05:00
William J. Bowman
9ec162b079
Added untested macro for defining inferrence rules
2015-01-21 01:37:50 -05:00
William J. Bowman
b57f2d4a85
STLC now works! Or, type-checks.
2015-01-20 00:56:18 -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
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
