suzanne.soy/cur
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Updates to the README

Browse Source
This commit is contained in:
William J. Bowman 2015-09-15 19:00:00 -04:00
parent 2796cba6fb
commit 34dd749be0
No known key found for this signature in database
GPG Key ID: DDD48D26958F0D1A
1 changed files with 8 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
README.md
View File

@ -19,15 +19,20 @@ Requires redex-lib version 1.6 if you want answers in a reasonable amount
of time. Otherwise, the type-checker may require exponential time
or worse.
Open up `stlc.rkt` to see an example of what advanced meta-programming can let you do.
Open up `examples/example.rkt` to see a tour of Cur's features.
Open up `examples/stlc.rkt` to see an example of what advanced meta-programming can let you do.
Open up `oll.rkt` to see the implementation of the meta-programs used to
enable `stlc.rkt`, including the parsers for BNF syntax and inference rule
enable `examples/stlc.rkt`, including the parsers for BNF syntax and inference rule
syntax, and Coq and LaTeX generators.
Open up `proofs-for-free.rkt` to see an implementation of the
Open up `examples/proofs-for-free.rkt` to see an implementation of the
translation defined in [Proofs for Free](http://staff.city.ac.uk/~ross/papers/proofs.html) as a meta-program.
Open up `stdlib/tactics` to see tactics, implemented entirely via
meta-programming.
Open up anything in `stdlib/` to see some standard dependent-type
formalisms.