| Wed, 06 Nov 2013 01:06:01 +0100 |
blanchet |
generalize more aggressively
|
file |
diff |
annotate
|
| Tue, 05 Nov 2013 16:47:10 +0100 |
blanchet |
get mutually recursive maps as well
|
file |
diff |
annotate
|
| Tue, 05 Nov 2013 13:23:27 +0100 |
blanchet |
fixed subtle name shadowing bug
|
file |
diff |
annotate
|
| Tue, 05 Nov 2013 12:40:58 +0100 |
blanchet |
use right permutation in 'map2'
|
file |
diff |
annotate
|
| Tue, 05 Nov 2013 11:55:45 +0100 |
blanchet |
stronger normalization, to increase n2m cache effectiveness
|
file |
diff |
annotate
|
| Tue, 05 Nov 2013 11:17:42 +0100 |
blanchet |
make local theory operations non-pervasive (makes more intuitive sense)
|
file |
diff |
annotate
|
| Tue, 05 Nov 2013 05:48:08 +0100 |
blanchet |
added some N2M caching
|
file |
diff |
annotate
|
| Tue, 05 Nov 2013 05:48:08 +0100 |
blanchet |
also generalize fixed types
|
file |
diff |
annotate
|
| Tue, 05 Nov 2013 05:48:08 +0100 |
blanchet |
generalize types when synthetizing n2m (co)recursors, to facilitate reuse
|
file |
diff |
annotate
|
| Tue, 05 Nov 2013 05:48:08 +0100 |
blanchet |
nicer error message in case of duplicates
|
file |
diff |
annotate
|
| Mon, 04 Nov 2013 15:44:43 +0100 |
blanchet |
better error handling
|
file |
diff |
annotate
|
| Mon, 04 Nov 2013 14:46:38 +0100 |
blanchet |
more robust n2m w.r.t. 'let's
|
file |
diff |
annotate
|
| Mon, 04 Nov 2013 11:03:13 +0100 |
blanchet |
made n2m code more robust w.r.t. advanced constructs (e.g. lambdas)
|
file |
diff |
annotate
|
| Mon, 04 Nov 2013 10:52:41 +0100 |
blanchet |
handle constructor syntax in n2m primcorec
|
file |
diff |
annotate
|
| Mon, 04 Nov 2013 10:52:41 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 04 Nov 2013 10:52:41 +0100 |
blanchet |
make code more robust w.r.t. applied/unapplied map (primrec vs. primcorec)
|
file |
diff |
annotate
|
| Mon, 21 Oct 2013 09:31:19 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Wed, 02 Oct 2013 16:29:40 +0200 |
blanchet |
don't register equations of the form 'f x = ...' as simp rules, even if they are safe (noncorecursive), because they unfold too aggresively concepts users are likely to want to stay folded
|
file |
diff |
annotate
|
| Tue, 01 Oct 2013 14:13:24 +0200 |
blanchet |
got rid of dead feature
|
file |
diff |
annotate
|
| Tue, 01 Oct 2013 14:05:25 +0200 |
blanchet |
renamed theory file
|
file |
diff |
annotate
|
| Sat, 28 Sep 2013 22:47:17 +0200 |
wenzelm |
make SML/NJ more happy;
|
file |
diff |
annotate
|
| Tue, 24 Sep 2013 00:01:10 +0200 |
blanchet |
register codatatypes with Nitpick
|
file |
diff |
annotate
|
| Fri, 20 Sep 2013 11:44:30 +0200 |
blanchet |
have "datatype_new_compat" register induction and recursion theorems in nested case
|
file |
diff |
annotate
|
| Tue, 17 Sep 2013 01:09:51 +0200 |
blanchet |
return right theorems
|
file |
diff |
annotate
|
| Fri, 13 Sep 2013 02:26:59 +0200 |
blanchet |
don't wrongly destroy sum types in coiterators
|
file |
diff |
annotate
|
| Mon, 09 Sep 2013 14:22:11 +0200 |
blanchet |
include map theorems in datastructure for "primcorec"
|
file |
diff |
annotate
|
| Mon, 09 Sep 2013 13:47:58 +0200 |
blanchet |
enriched data structure with necessary theorems
|
file |
diff |
annotate
|
| Fri, 30 Aug 2013 11:27:23 +0200 |
blanchet |
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
|
file |
diff |
annotate
|