| Wed, 25 Sep 2013 16:43:46 +0200 |
blanchet |
killed redundant argument
|
file |
diff |
annotate
|
| Wed, 25 Sep 2013 14:21:18 +0200 |
blanchet |
move useful functions to library
|
file |
diff |
annotate
|
| Wed, 25 Sep 2013 13:39:34 +0200 |
panny |
merge
|
file |
diff |
annotate
|
| Wed, 25 Sep 2013 12:43:20 +0200 |
panny |
simplified code
|
file |
diff |
annotate
|
| Wed, 25 Sep 2013 00:38:13 +0200 |
panny |
add non-corecursive constructor view theorems to simps
|
file |
diff |
annotate
|
| Wed, 25 Sep 2013 12:29:06 +0200 |
blanchet |
more powerful fold
|
file |
diff |
annotate
|
| Tue, 24 Sep 2013 22:21:51 +0200 |
blanchet |
commented out debugging output in "primcorec"
|
file |
diff |
annotate
|
| Tue, 24 Sep 2013 20:40:36 +0200 |
blanchet |
started adding support for "nat_case" as case study for all "case" constructs
|
file |
diff |
annotate
|
| Tue, 24 Sep 2013 18:07:09 +0200 |
panny |
support "of" syntax to disambiguate selector equations
|
file |
diff |
annotate
|
| Tue, 24 Sep 2013 17:54:09 +0200 |
blanchet |
don't note more induction principles than there are functions + tuning
|
file |
diff |
annotate
|
| Tue, 24 Sep 2013 15:16:59 +0200 |
panny |
add "primcorec" command (cf. ae7f50e70c09)
|
file |
diff |
annotate
|
| Tue, 24 Sep 2013 00:18:22 +0200 |
blanchet |
set code and nitpick_simp attributes on primcorec theorems
|
file |
diff |
annotate
|
| Mon, 23 Sep 2013 10:58:37 +0200 |
blanchet |
note coinduct theorems in "primcorec"
|
file |
diff |
annotate
|
| Mon, 23 Sep 2013 10:45:26 +0200 |
blanchet |
generate "simps" from "primcorec"
|
file |
diff |
annotate
|
| Mon, 23 Sep 2013 10:38:23 +0200 |
blanchet |
undid copy-paste
|
file |
diff |
annotate
|
| Mon, 23 Sep 2013 10:34:10 +0200 |
blanchet |
avoid giving same name to simplifying constructor as to real one (to avoid risks of confusion when reading the code)
|
file |
diff |
annotate
|
| Mon, 23 Sep 2013 10:30:43 +0200 |
blanchet |
tuned code
|
file |
diff |
annotate
|
| Fri, 20 Sep 2013 16:32:27 +0200 |
blanchet |
renamed "primcorec" to "primcorecursive", to open the door to a 'theory -> theory' command called "primcorec" (cf. "fun" vs. "function")
|
file |
diff |
annotate
|
| Fri, 20 Sep 2013 00:08:42 +0200 |
blanchet |
setting the stage for safe constructor simp rules
|
file |
diff |
annotate
|
| Thu, 19 Sep 2013 23:54:54 +0200 |
blanchet |
added TODO
|
file |
diff |
annotate
|
| Thu, 19 Sep 2013 17:38:03 +0200 |
traytel |
don't declare ctr view primcorec theorems as simp (they loop)
|
file |
diff |
annotate
|
| Thu, 19 Sep 2013 16:12:43 +0200 |
panny |
simplified code; eliminated some dummyTs
|
file |
diff |
annotate
|
| Thu, 19 Sep 2013 12:20:12 +0200 |
blanchet |
avoid infinite loop for unapplied terms + tuning
|
file |
diff |
annotate
|
| Thu, 19 Sep 2013 11:27:32 +0200 |
blanchet |
generalize code to handle zero-argument case gracefully (e.g. for nullay functions defined over codatatypes that corecurse through "fun"
|
file |
diff |
annotate
|
| Thu, 19 Sep 2013 01:09:25 +0200 |
blanchet |
simplified code
|
file |
diff |
annotate
|
| Thu, 19 Sep 2013 00:32:33 +0200 |
panny |
generate more theorems (e.g. for types with only one constructor)
|
file |
diff |
annotate
|
| Wed, 18 Sep 2013 22:59:11 +0200 |
panny |
generate constructor view theorems
|
file |
diff |
annotate
|
| Wed, 18 Sep 2013 18:12:40 +0200 |
blanchet |
tuned tactics
|
file |
diff |
annotate
|
| Wed, 18 Sep 2013 15:33:32 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 16 Sep 2013 15:03:23 +0200 |
panny |
prove simp theorems for newly generated definitions
|
file |
diff |
annotate
|