William J. Bowman
024f4e188e
Fixed reduction of (elim ==)
...
Fixed eliminator reduction, at least for the == type. Code currently
does the minimum required to make #23 work, but may have introduced bugs
in the process.
2015-09-26 00:57:36 -04:00
William J. Bowman
473394ccc1
Try hard to figure out parameters
...
Previously just assumed an inductive could only return a universe, and
everything else was parameters. This was stupid.
Now tries to figure out parameters based on the return type of the
constructors. This allows the example from #23 to type check.
2015-09-26 00:17:19 -04:00
William J. Bowman
8aabbc219b
disabled test that cause setup errors
2015-09-25 20:10:32 -04:00
William J. Bowman
e54c7e5bb5
Added query-type command to sugar
2015-09-25 20:08:07 -04:00
William J. Bowman
ff2f052a21
More unicode in stdlib/sugar
...
closes #21
2015-09-25 19:44:37 -04:00
William J. Bowman
84359fc2fd
This is related to previous commit
2015-09-25 19:33:12 -04:00
William J. Bowman
f05be17fdf
Added Or, but can't seem to use it
2015-09-25 19:32:18 -04:00
William J. Bowman
4c9c6b4e60
Analyzed and documented eliminator reduction
2015-09-25 18:48:07 -04:00
William J. Bowman
aaaab38729
even? odd? and lots of tests
...
These tests reveal issue #20 , and it seems some other bug that causes an
infinite loop.
2015-09-25 18:36:27 -04:00
William J. Bowman
59226538d5
Expanded elim docs
2015-09-25 18:24:39 -04:00
William J. Bowman
f353ad8991
Fixed coq generator for elim
2015-09-25 18:08:20 -04:00
William J. Bowman
f4d38dec51
Recovered better elim syntax in sugar.rkt
2015-09-25 17:55:25 -04:00
William J. Bowman
9681fbd9e0
Restricted elim curnel syntax
...
The curnel was documented as having a restricted syntax, but this was
not actually enforced. Now it is.
2015-09-25 17:50:27 -04:00
William J. Bowman
b64d20319f
Updated documentation and examples to new elim
2015-09-25 17:50:03 -04:00
William J. Bowman
de3a4d9cf3
Merge branch 'typing-elim'
...
Closes #6
2015-09-25 17:25:12 -04:00
William J. Bowman
8ba4ed17d9
Fixed bug in reduction of elim
...
elim was not checking that the arguments to be used for the parameters
of the inductive matched the actual parameters expected, resulting in
incorrect and non-deterministic unification, and thus incorrect
reduction when the parameters were unified incorrectly.
2015-09-25 16:52:49 -04:00
William J. Bowman
2666080278
Removed dead code
2015-09-25 15:16:44 -04:00
William J. Bowman
bd795ba0ea
Tests reveal type-safety is broken for elim
2015-09-25 14:49:47 -04:00
William J. Bowman
1fd96f0140
Proof read sartactics. closes #17
2015-09-25 13:54:42 -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
d82727a3fb
Starting fixing uses of elim, but there is a bug
2015-09-24 13:51:29 -04:00
William J. Bowman
4bb6dc3c71
Tweaks to README
2015-09-23 21:41:04 -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
9055662a5d
Exported some convenience features
2015-09-23 16:22:05 -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
c5eb2ff2af
Add more boolean stuff
2015-09-22 23:32:57 -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
e4bf99c277
Syntax parse for better error messages
2015-09-22 22:59:07 -04:00
William J. Bowman
eeb2b9182a
Updated README
2015-09-22 18:55:14 -04:00
William J. Bowman
bfc72d8fd3
Documented reflection features
2015-09-22 18:18:26 -04:00
William J. Bowman
41b40fea2b
Commented out things that cause package to fail
...
Lots of tests and examples cause the package to fail to build. These
have been commented out until they can be fixed.
2015-09-22 15:32:54 -04:00
William J. Bowman
a3094b55bb
Fixed top
2015-09-22 15:32:45 -04:00
William J. Bowman
722ac7d68f
Added missing dependency
2015-09-22 15:30:00 -04:00
William J. Bowman
f73f4a2c98
Finished documenting curnel forms
2015-09-22 15:29:49 -04:00
William J. Bowman
8681282ef9
Added top-interactive support/fixed top-level eval
...
Also fixed some random stylistic things
2015-09-22 14:06:03 -04:00
William J. Bowman
0f5026aee0
Fixed typo
2015-09-16 19:54:16 -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
56abd36a65
Added disclaimer
2015-09-16 12:44:56 -04:00
William J. Bowman
3b5aafdf69
Updated install instructions
2015-09-16 12:41:54 -04:00
