| Fri, 26 Mar 2010 10:55:13 +0100 |
Cezary Kaliszyk |
Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
|
file |
diff |
annotate
|
| Wed, 24 Mar 2010 12:53:39 +0100 |
Christian Urban |
some tuning; possible fix for strange paper generation
|
file |
diff |
annotate
|
| Tue, 23 Mar 2010 09:05:23 +0100 |
Cezary Kaliszyk |
More reorganization.
|
file |
diff |
annotate
|
| Tue, 23 Mar 2010 08:51:43 +0100 |
Cezary Kaliszyk |
Move Leroy out of Test, rename accordingly.
|
file |
diff |
annotate
|
| Tue, 23 Mar 2010 08:46:44 +0100 |
Cezary Kaliszyk |
Term1 is identical to Example 3
|
file |
diff |
annotate
|
| Tue, 23 Mar 2010 08:45:08 +0100 |
Cezary Kaliszyk |
Move example3 out.
|
file |
diff |
annotate
|
| Tue, 23 Mar 2010 08:42:02 +0100 |
Cezary Kaliszyk |
Move Ex1 and Ex2 out of Test
|
file |
diff |
annotate
|
| Tue, 23 Mar 2010 08:33:48 +0100 |
Cezary Kaliszyk |
Move examples which create more permutations out
|
file |
diff |
annotate
|
| Tue, 23 Mar 2010 08:22:48 +0100 |
Cezary Kaliszyk |
Move LamEx out of Test.
|
file |
diff |
annotate
|
| Tue, 23 Mar 2010 08:11:11 +0100 |
Cezary Kaliszyk |
Move Non-respectful examples to NotRsp
|
file |
diff |
annotate
|
| Tue, 23 Mar 2010 07:04:27 +0100 |
Cezary Kaliszyk |
Move the comment to appropriate place.
|
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 15:01:01 +0100 |
Cezary Kaliszyk |
Update Test to use fset.
|
file |
diff |
annotate
|
| Thu, 18 Mar 2010 19:02:33 +0100 |
Cezary Kaliszyk |
Leroy96 supp=fv and fixes to make it compile
|
file |
diff |
annotate
|
| Thu, 18 Mar 2010 16:22:10 +0100 |
Christian Urban |
corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant
|
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 10:12:41 +0100 |
Cezary Kaliszyk |
Which proofs need a 'sorry'.
|
file |
diff |
annotate
|
| Thu, 18 Mar 2010 10:02:21 +0100 |
Christian Urban |
vixed variable names
|
file |
diff |
annotate
|
| Thu, 18 Mar 2010 09:31:31 +0100 |
Christian Urban |
simplified strong induction proof by using flip
|
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
|
| Wed, 17 Mar 2010 17:11:23 +0100 |
Christian Urban |
merged
|
file |
diff |
annotate
|
| Wed, 17 Mar 2010 15:13:03 +0100 |
Christian Urban |
added partial proof for the strong induction principle
|
file |
diff |
annotate
|
| Wed, 17 Mar 2010 12:23:04 +0100 |
Cezary Kaliszyk |
merge
|
file |
diff |
annotate
|
| Wed, 17 Mar 2010 12:18:35 +0100 |
Cezary Kaliszyk |
cheat_alpha_eqvt no longer needed. Cleaned the tracing messages.
|
file |
diff |
annotate
|
| Wed, 17 Mar 2010 11:53:56 +0100 |
Christian Urban |
added proof of supp/fv for type schemes
|
file |
diff |
annotate
|
| Wed, 17 Mar 2010 10:34:25 +0100 |
Christian Urban |
added partial proof of supp for type schemes
|
file |
diff |
annotate
|
| Wed, 17 Mar 2010 09:57:54 +0100 |
Cezary Kaliszyk |
Fix in alpha; support of the recursive Let works :)
|
file |
diff |
annotate
|
| Wed, 17 Mar 2010 09:42:56 +0100 |
Cezary Kaliszyk |
The recursive supp just has one equation too much.
|
file |
diff |
annotate
|