Sat, 21 Dec 2013 09:44:28 +0100 |
blanchet |
renamed 'exhaust' to 'nchotomy' since it's expressed in the object logic (cf. datatype package)
|
file |
diff |
annotate
|
Fri, 20 Dec 2013 11:34:07 +0100 |
blanchet |
note manually proved exclusiveness property
|
file |
diff |
annotate
|
Fri, 20 Dec 2013 11:12:51 +0100 |
blanchet |
note exhaust proof obligation
|
file |
diff |
annotate
|
Thu, 19 Dec 2013 21:49:30 +0100 |
blanchet |
implemented 'exhaustive' option in tactic
|
file |
diff |
annotate
|
Wed, 18 Dec 2013 14:50:25 +0100 |
panny |
pass down user input in more cases in order to preserve "let"s etc.
|
file |
diff |
annotate
|
Wed, 18 Dec 2013 14:06:34 +0100 |
panny |
pass auto-proved exhaustiveness properties to tactic;
|
file |
diff |
annotate
|
Mon, 02 Dec 2013 19:49:34 +0100 |
panny |
generate "code" theorems for incomplete definitions
|
file |
diff |
annotate
|
Sun, 01 Dec 2013 19:32:57 +0100 |
panny |
more work towards "exhaustive"
|
file |
diff |
annotate
|
Mon, 25 Nov 2013 20:25:22 +0100 |
panny |
prevent exception when equations for a function are missing;
|
file |
diff |
annotate
|
Wed, 06 Nov 2013 13:00:45 +0100 |
blanchet |
removed dead code
|
file |
diff |
annotate
|
Wed, 06 Nov 2013 12:47:50 +0100 |
blanchet |
take out possibility of moving corecursive calls past constructors -- this doesn't work in the general case
|
file |
diff |
annotate
|
Tue, 05 Nov 2013 16:53:40 +0100 |
blanchet |
avoid subtle failure in the presence of top sort
|
file |
diff |
annotate
|
Tue, 05 Nov 2013 16:47:10 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
Mon, 04 Nov 2013 16:53:43 +0100 |
blanchet |
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
|
file |
diff |
annotate
| base
|