| Wed, 03 Feb 2010 12:58:02 +0100 |
Christian Urban |
another adaptation for the eqvt-change
|
file |
diff |
annotate
|
| Wed, 03 Feb 2010 12:11:23 +0100 |
Cezary Kaliszyk |
The alpha-equivalence relation for let-rec. Not sure if correct...
|
file |
diff |
annotate
|
| Tue, 02 Feb 2010 13:10:46 +0100 |
Cezary Kaliszyk |
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
|
file |
diff |
annotate
|
| Tue, 02 Feb 2010 10:43:48 +0100 |
Cezary Kaliszyk |
With induct instead of induct_tac, just one induction is sufficient.
|
file |
diff |
annotate
|
| Tue, 02 Feb 2010 10:20:54 +0100 |
Cezary Kaliszyk |
General alpha_gen_trans for one-variable abstraction.
|
file |
diff |
annotate
|
| Mon, 01 Feb 2010 11:39:59 +0100 |
Cezary Kaliszyk |
The current state of fv vs supp proofs in LF.
|
file |
diff |
annotate
|
| Mon, 01 Feb 2010 11:16:13 +0100 |
Cezary Kaliszyk |
More proofs in the LF example.
|
file |
diff |
annotate
|
| Mon, 01 Feb 2010 09:56:32 +0100 |
Cezary Kaliszyk |
Ported LF to the generic lambda and solved the simpler _supp cases.
|
file |
diff |
annotate
|