William J. Bowman
b853d49b31
Fixed some tactic docs; tests that print to stdout
2015-10-03 03:55:22 -04:00
William J. Bowman
822c114f62
Fixed prop; removed define-theorem and qed macros
...
These macros were not really serving a good purpose. They were defined
early on to demonstrate that metaprogramming can give us Coq-like
notation, but really, we have much more interesting demos.
2015-10-03 03:33:12 -04:00
William J. Bowman
ca9e36a973
Added unicode to docs
2015-10-02 21:38:43 -04:00
William J. Bowman
a80c4a162f
Added a fancy let form
2015-10-02 21:14:23 -04:00
William J. Bowman
cf6f81fbd4
Added single step evaluation abilities. Closes #27
...
* Added single step meta-function to core
* Expose step/syn in redex-lang
* Added macro to sugar for convenience use
* Updated relevant docs (also fixed bug in reflection docs)
2015-09-29 15:41:21 -04:00
William J. Bowman
e54c7e5bb5
Added query-type command to sugar
2015-09-25 20:08:07 -04:00
William J. Bowman
59226538d5
Expanded elim docs
2015-09-25 18:24:39 -04:00
William J. Bowman
f4d38dec51
Recovered better elim syntax in sugar.rkt
2015-09-25 17:55:25 -04:00
William J. Bowman
b64d20319f
Updated documentation and examples to new elim
2015-09-25 17:50:03 -04:00
William J. Bowman
1261ef2b73
Fixed some bugs introduced by changes to sugar
...
Yesterday's changes to sugar broke some things:
* case isn't smart enough to infer the right things in all cases yet, so
added previously existing case* for when it is necessary.
* reexport define-theorem and qed from sugar, since still used in prop.
2015-09-25 13:37:51 -04:00
William J. Bowman
bf867bca7f
Moved some features out of curnel
...
* run is user-definable through the existing reflection features; moved
to sugar.
* define need not have special function support in curnel; moved to
sugar.
* fixed relevant documentation
2015-09-25 13:36:44 -04:00
William J. Bowman
2477fe9f4b
Made case macro do more work
...
Now the case macro is closer to a pattern-matcher.
2015-09-24 18:01:42 -04:00
William J. Bowman
52ec79f61b
Documented sugar
2015-09-24 17:51:38 -04:00
William J. Bowman
fa9389ee7f
Hacks to make cur work in the REPL
...
Look I don't want to talk about it, but now you can use Cur in DrRacket.
Closes #18
2015-09-23 21:35:27 -04:00
William J. Bowman
ac081577a0
Fixed scribbled inline TODOs
2015-09-23 18:11:08 -04:00
William J. Bowman
d2642b1c38
Fixed typo
2015-09-23 18:08:15 -04:00
William J. Bowman
edea1909ec
Documented the OLL
2015-09-23 17:58:54 -04:00
William J. Bowman
c68d0ae97a
Added a few examples to tactic docs
2015-09-23 16:40:23 -04:00
William J. Bowman
a4ca0c5671
Documentation for tactics complete
2015-09-23 16:20:37 -04:00
William J. Bowman
aa4b0ccf82
Started documenting the tactics library
2015-09-23 00:11:21 -04:00
William J. Bowman
fae24ab496
Styles tweaks
...
* Types now start with a Capital letter, because.
* Boolean expression no longer start with the letter b.
2015-09-22 23:32:02 -04:00
William J. Bowman
d177577ac9
Fixed TODO thing
2015-09-22 23:30:00 -04:00
William J. Bowman
31f4673477
Added missing scribble aux defs
2015-09-22 23:25:33 -04:00
William J. Bowman
bfc72d8fd3
Documented reflection features
2015-09-22 18:18:26 -04:00
William J. Bowman
f73f4a2c98
Finished documenting curnel forms
2015-09-22 15:29:49 -04:00
William J. Bowman
a9e042967e
More work on docs
2015-09-16 19:54:06 -04:00
William J. Bowman
a787f974da
Starting scribbling
2015-09-16 16:05:29 -04:00
William J. Bowman
740aaee756
cur is now a pkg and a #lang
...
These features are currently undocumented.
2015-09-16 12:25:22 -04:00
