| Sat, 20 Mar 2010 09:27:28 +0100 |
Cezary Kaliszyk |
Use 'alpha_bn_refl' to get rid of one of the sorrys.
|
file |
diff |
annotate
|
| Fri, 19 Mar 2010 18:42:57 +0100 |
Cezary Kaliszyk |
Automatically derive support for datatypes with at-most one binding per constructor.
|
file |
diff |
annotate
|
| Fri, 19 Mar 2010 14:54:30 +0100 |
Cezary Kaliszyk |
Use fs typeclass in showing finite support + some cheat cleaning.
|
file |
diff |
annotate
|
| Thu, 18 Mar 2010 15:13:20 +0100 |
Cezary Kaliszyk |
Rename "_property" to ".property"
|
file |
diff |
annotate
|
| Thu, 18 Mar 2010 12:09:59 +0100 |
Cezary Kaliszyk |
Added fv,bn,distinct,perm to the simplifier.
|
file |
diff |
annotate
|
| Thu, 18 Mar 2010 08:32:55 +0100 |
Cezary Kaliszyk |
Rename bound variables + minor cleaning.
|
file |
diff |
annotate
|
| Thu, 18 Mar 2010 07:43:44 +0100 |
Cezary Kaliszyk |
Prove pseudo-inject (eq-iff) on the exported level and rename appropriately.
|
file |
diff |
annotate
|
| Tue, 16 Mar 2010 15:27:47 +0100 |
Cezary Kaliszyk |
FV_bn generated for recursive functions as well, and used in main fv for bindings.
|
file |
diff |
annotate
|
| Mon, 15 Mar 2010 10:36:09 +0100 |
Cezary Kaliszyk |
LF works with new alpha...?
|
file |
diff |
annotate
|
| Thu, 11 Mar 2010 17:49:07 +0100 |
Cezary Kaliszyk |
Finite_support proof no longer needed in LF.
|
file |
diff |
annotate
|
| Mon, 08 Mar 2010 11:12:15 +0100 |
Cezary Kaliszyk |
More fine-grained nominal restriction for debugging.
|
file |
diff |
annotate
|
| Fri, 05 Mar 2010 17:09:48 +0100 |
Cezary Kaliszyk |
Ported LF to the parser interface.
|
file |
diff |
annotate
|
| Fri, 05 Mar 2010 10:23:40 +0100 |
Cezary Kaliszyk |
Fixed LF for one quantifier over 2 premises.
|
file |
diff |
annotate
|
| Tue, 02 Mar 2010 15:12:50 +0100 |
Cezary Kaliszyk |
Minor
|
file |
diff |
annotate
|
| Tue, 02 Mar 2010 11:04:49 +0100 |
Cezary Kaliszyk |
Fixed eqvt code.
|
file |
diff |
annotate
|
| Fri, 26 Feb 2010 15:42:00 +0100 |
Cezary Kaliszyk |
RSP of perms can be shown in one go.
|
file |
diff |
annotate
|
| Fri, 26 Feb 2010 15:10:55 +0100 |
Cezary Kaliszyk |
Change in signature of prove_const_rsp for general lifting.
|
file |
diff |
annotate
|
| Fri, 26 Feb 2010 13:57:43 +0100 |
Cezary Kaliszyk |
Permutation and FV_Alpha interface change.
|
file |
diff |
annotate
|
| Thu, 25 Feb 2010 12:15:11 +0100 |
Cezary Kaliszyk |
Code for proving eqvt, still in Terms.
|
file |
diff |
annotate
|
| Thu, 25 Feb 2010 07:48:57 +0100 |
Christian Urban |
merged
|
file |
diff |
annotate
| base
|
| Thu, 25 Feb 2010 07:48:33 +0100 |
Christian Urban |
moved Nominal to "toplevel"
|
file |
diff |
annotate
| base
|