2010-03-26 |
Cezary Kaliszyk |
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
|
file |
diff |
annotate
|
2010-03-24 |
Christian Urban |
some tuning; possible fix for strange paper generation
|
file |
diff |
annotate
|
2010-03-23 |
Cezary Kaliszyk |
More reorganization.
|
file |
diff |
annotate
|
2010-03-23 |
Cezary Kaliszyk |
Move Leroy out of Test, rename accordingly.
|
file |
diff |
annotate
|
2010-03-23 |
Cezary Kaliszyk |
Term1 is identical to Example 3
|
file |
diff |
annotate
|
2010-03-23 |
Cezary Kaliszyk |
Move example3 out.
|
file |
diff |
annotate
|
2010-03-23 |
Cezary Kaliszyk |
Move Ex1 and Ex2 out of Test
|
file |
diff |
annotate
|
2010-03-23 |
Cezary Kaliszyk |
Move examples which create more permutations out
|
file |
diff |
annotate
|
2010-03-23 |
Cezary Kaliszyk |
Move LamEx out of Test.
|
file |
diff |
annotate
|
2010-03-23 |
Cezary Kaliszyk |
Move Non-respectful examples to NotRsp
|
file |
diff |
annotate
|
2010-03-23 |
Cezary Kaliszyk |
Move the comment to appropriate place.
|
file |
diff |
annotate
|
2010-03-19 |
Cezary Kaliszyk |
Automatically derive support for datatypes with at-most one binding per constructor.
|
file |
diff |
annotate
|
2010-03-19 |
Cezary Kaliszyk |
Update Test to use fset.
|
file |
diff |
annotate
|
2010-03-18 |
Cezary Kaliszyk |
Leroy96 supp=fv and fixes to make it compile
|
file |
diff |
annotate
|
2010-03-18 |
Christian Urban |
corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant
|
file |
diff |
annotate
|
2010-03-18 |
Cezary Kaliszyk |
Rename "_property" to ".property"
|
file |
diff |
annotate
|
2010-03-18 |
Cezary Kaliszyk |
Added fv,bn,distinct,perm to the simplifier.
|
file |
diff |
annotate
|
2010-03-18 |
Cezary Kaliszyk |
Which proofs need a 'sorry'.
|
file |
diff |
annotate
|
2010-03-18 |
Christian Urban |
vixed variable names
|
file |
diff |
annotate
|
2010-03-18 |
Christian Urban |
simplified strong induction proof by using flip
|
file |
diff |
annotate
|
2010-03-18 |
Cezary Kaliszyk |
Rename bound variables + minor cleaning.
|
file |
diff |
annotate
|
2010-03-18 |
Cezary Kaliszyk |
Prove pseudo-inject (eq-iff) on the exported level and rename appropriately.
|
file |
diff |
annotate
|
2010-03-17 |
Christian Urban |
merged
|
file |
diff |
annotate
|
2010-03-17 |
Christian Urban |
added partial proof for the strong induction principle
|
file |
diff |
annotate
|
2010-03-17 |
Cezary Kaliszyk |
merge
|
file |
diff |
annotate
|
2010-03-17 |
Cezary Kaliszyk |
cheat_alpha_eqvt no longer needed. Cleaned the tracing messages.
|
file |
diff |
annotate
|
2010-03-17 |
Christian Urban |
added proof of supp/fv for type schemes
|
file |
diff |
annotate
|
2010-03-17 |
Christian Urban |
added partial proof of supp for type schemes
|
file |
diff |
annotate
|
2010-03-17 |
Cezary Kaliszyk |
Fix in alpha; support of the recursive Let works :)
|
file |
diff |
annotate
|
2010-03-17 |
Cezary Kaliszyk |
The recursive supp just has one equation too much.
|
file |
diff |
annotate
|