Mercurial Mercurial > hg > nominal2 / changelog
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
(0) -1000 -300 -100 -60 +60 +100 +300 +1000 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Thu, 18 Mar 2010 15:32:49 +0100 Continued description of alpha.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Mar 2010 15:32:49 +0100] rev 1516
Continued description of alpha.
Thu, 18 Mar 2010 15:13:20 +0100 Rename "_property" to ".property"
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Mar 2010 15:13:20 +0100] rev 1515
Rename "_property" to ".property"
Thu, 18 Mar 2010 14:48:27 +0100 First part of the description of alpha_ty.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Mar 2010 14:48:27 +0100] rev 1514
First part of the description of alpha_ty.
Thu, 18 Mar 2010 14:29:42 +0100 Description of generation of alpha_bn.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Mar 2010 14:29:42 +0100] rev 1513
Description of generation of alpha_bn.
Thu, 18 Mar 2010 14:05:49 +0100 case names also for _induct
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Mar 2010 14:05:49 +0100] rev 1512
case names also for _induct
Thu, 18 Mar 2010 12:32:03 +0100 Case_Names for _inducts. Does not work for _induct yet.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Mar 2010 12:32:03 +0100] rev 1511
Case_Names for _inducts. Does not work for _induct yet.
Thu, 18 Mar 2010 12:09:59 +0100 Added fv,bn,distinct,perm to the simplifier.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Mar 2010 12:09:59 +0100] rev 1510
Added fv,bn,distinct,perm to the simplifier.
Thu, 18 Mar 2010 11:37:10 +0100 merge
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Mar 2010 11:37:10 +0100] rev 1509
merge
Thu, 18 Mar 2010 11:36:03 +0100 Simplified the description.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Mar 2010 11:36:03 +0100] rev 1508
Simplified the description.
Thu, 18 Mar 2010 11:33:56 +0100 merged
changeset
Christian Urban <urbanc@in.tum.de> [Thu, 18 Mar 2010 11:33:56 +0100] rev 1507
merged
Thu, 18 Mar 2010 11:33:37 +0100 slightly more in the paper
changeset
Christian Urban <urbanc@in.tum.de> [Thu, 18 Mar 2010 11:33:37 +0100] rev 1506
slightly more in the paper
Thu, 18 Mar 2010 11:29:12 +0100 Update the description of the generation of fv function.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Mar 2010 11:29:12 +0100] rev 1505
Update the description of the generation of fv function.
Thu, 18 Mar 2010 11:16:53 +0100 fv_bn may need to call other fv_bns.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Mar 2010 11:16:53 +0100] rev 1504
fv_bn may need to call other fv_bns.
Thu, 18 Mar 2010 10:15:57 +0100 Update TODO.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Mar 2010 10:15:57 +0100] rev 1503
Update TODO.
Thu, 18 Mar 2010 10:12:41 +0100 Which proofs need a 'sorry'.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Mar 2010 10:12:41 +0100] rev 1502
Which proofs need a 'sorry'.
Thu, 18 Mar 2010 10:05:36 +0100 added TODO
changeset
Christian Urban <urbanc@in.tum.de> [Thu, 18 Mar 2010 10:05:36 +0100] rev 1501
added TODO
Thu, 18 Mar 2010 10:02:21 +0100 vixed variable names
changeset
Christian Urban <urbanc@in.tum.de> [Thu, 18 Mar 2010 10:02:21 +0100] rev 1500
vixed variable names
Thu, 18 Mar 2010 09:31:31 +0100 simplified strong induction proof by using flip
changeset
Christian Urban <urbanc@in.tum.de> [Thu, 18 Mar 2010 09:31:31 +0100] rev 1499
simplified strong induction proof by using flip
Thu, 18 Mar 2010 08:32:55 +0100 Rename bound variables + minor cleaning.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Mar 2010 08:32:55 +0100] rev 1498
Rename bound variables + minor cleaning.
Thu, 18 Mar 2010 08:03:42 +0100 Move most of the exporting out of the parser.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Mar 2010 08:03:42 +0100] rev 1497
Move most of the exporting out of the parser.
Thu, 18 Mar 2010 07:43:44 +0100 Prove pseudo-inject (eq-iff) on the exported level and rename appropriately.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Mar 2010 07:43:44 +0100] rev 1496
Prove pseudo-inject (eq-iff) on the exported level and rename appropriately.
Thu, 18 Mar 2010 07:35:44 +0100 Prove eqvts on exported terms.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Mar 2010 07:35:44 +0100] rev 1495
Prove eqvts on exported terms.
Thu, 18 Mar 2010 07:26:36 +0100 Clean 'Lift', start working only on exported things in Parser.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Mar 2010 07:26:36 +0100] rev 1494
Clean 'Lift', start working only on exported things in Parser.
Thu, 18 Mar 2010 00:17:21 +0100 slightly more of the paper
changeset
Christian Urban <urbanc@in.tum.de> [Thu, 18 Mar 2010 00:17:21 +0100] rev 1493
slightly more of the paper
Wed, 17 Mar 2010 20:42:42 +0100 merged
changeset
Christian Urban <urbanc@in.tum.de> [Wed, 17 Mar 2010 20:42:42 +0100] rev 1492
merged
Wed, 17 Mar 2010 20:42:22 +0100 paper uses now a heap file - does not compile so long anymore
changeset
Christian Urban <urbanc@in.tum.de> [Wed, 17 Mar 2010 20:42:22 +0100] rev 1491
paper uses now a heap file - does not compile so long anymore
Wed, 17 Mar 2010 18:53:23 +0100 merge
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Mar 2010 18:53:23 +0100] rev 1490
merge
Wed, 17 Mar 2010 18:52:59 +0100 compose_sym2 works also for term5
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Mar 2010 18:52:59 +0100] rev 1489
compose_sym2 works also for term5
Wed, 17 Mar 2010 17:59:04 +0100 Updated Term1, including statement of strong induction.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Mar 2010 17:59:04 +0100] rev 1488
Updated Term1, including statement of strong induction.
Wed, 17 Mar 2010 17:40:14 +0100 Proper compose_sym2
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Mar 2010 17:40:14 +0100] rev 1487
Proper compose_sym2
Wed, 17 Mar 2010 17:11:23 +0100 merged
changeset
Christian Urban <urbanc@in.tum.de> [Wed, 17 Mar 2010 17:11:23 +0100] rev 1486
merged
Wed, 17 Mar 2010 17:10:19 +0100 temporarily disabled tests in Nominal/ROOT
changeset
Christian Urban <urbanc@in.tum.de> [Wed, 17 Mar 2010 17:10:19 +0100] rev 1485
temporarily disabled tests in Nominal/ROOT
Wed, 17 Mar 2010 15:13:31 +0100 made paper to compile
changeset
Christian Urban <urbanc@in.tum.de> [Wed, 17 Mar 2010 15:13:31 +0100] rev 1484
made paper to compile
Wed, 17 Mar 2010 15:13:03 +0100 added partial proof for the strong induction principle
changeset
Christian Urban <urbanc@in.tum.de> [Wed, 17 Mar 2010 15:13:03 +0100] rev 1483
added partial proof for the strong induction principle
Wed, 17 Mar 2010 17:09:01 +0100 Trying to find a compose lemma for 2 arguments.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Mar 2010 17:09:01 +0100] rev 1482
Trying to find a compose lemma for 2 arguments.
Wed, 17 Mar 2010 12:23:04 +0100 merge
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Mar 2010 12:23:04 +0100] rev 1481
merge
Wed, 17 Mar 2010 12:18:35 +0100 cheat_alpha_eqvt no longer needed. Cleaned the tracing messages.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Mar 2010 12:18:35 +0100] rev 1480
cheat_alpha_eqvt no longer needed. Cleaned the tracing messages.
Wed, 17 Mar 2010 11:54:22 +0100 merged
changeset
Christian Urban <urbanc@in.tum.de> [Wed, 17 Mar 2010 11:54:22 +0100] rev 1479
merged
Wed, 17 Mar 2010 11:53:56 +0100 added proof of supp/fv for type schemes
changeset
Christian Urban <urbanc@in.tum.de> [Wed, 17 Mar 2010 11:53:56 +0100] rev 1478
added proof of supp/fv for type schemes
Wed, 17 Mar 2010 11:40:58 +0100 Updated Type Schemes to automatic lifting. One goal is not true because of the restriction.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Mar 2010 11:40:58 +0100] rev 1477
Updated Type Schemes to automatic lifting. One goal is not true because of the restriction.
Wed, 17 Mar 2010 11:20:24 +0100 Remove Term5a, since it is now identical to Term5.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Mar 2010 11:20:24 +0100] rev 1476
Remove Term5a, since it is now identical to Term5.
Wed, 17 Mar 2010 11:11:42 +0100 merge
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Mar 2010 11:11:42 +0100] rev 1475
merge
Wed, 17 Mar 2010 11:11:25 +0100 Finished all proofs in Term5 and Term5n.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Mar 2010 11:11:25 +0100] rev 1474
Finished all proofs in Term5 and Term5n.
Wed, 17 Mar 2010 10:34:25 +0100 added partial proof of supp for type schemes
changeset
Christian Urban <urbanc@in.tum.de> [Wed, 17 Mar 2010 10:34:25 +0100] rev 1473
added partial proof of supp for type schemes
Wed, 17 Mar 2010 09:57:54 +0100 Fix in alpha; support of the recursive Let works :)
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Mar 2010 09:57:54 +0100] rev 1472
Fix in alpha; support of the recursive Let works :)
Wed, 17 Mar 2010 09:42:56 +0100 The recursive supp just has one equation too much.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Mar 2010 09:42:56 +0100] rev 1471
The recursive supp just has one equation too much.
Wed, 17 Mar 2010 09:25:01 +0100 Fix for the change of alpha_gen.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Mar 2010 09:25:01 +0100] rev 1470
Fix for the change of alpha_gen.
Wed, 17 Mar 2010 09:18:27 +0100 merge
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Mar 2010 09:18:27 +0100] rev 1469
merge
Wed, 17 Mar 2010 09:17:55 +0100 Generate compound FV and Alpha for recursive bindings.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Mar 2010 09:17:55 +0100] rev 1468
Generate compound FV and Alpha for recursive bindings.
Wed, 17 Mar 2010 08:39:46 +0100 Lifting theorems with compound fv and compound alpha.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Mar 2010 08:39:46 +0100] rev 1467
Lifting theorems with compound fv and compound alpha.
Wed, 17 Mar 2010 08:07:25 +0100 commented out examples that should not work; but for example type-scheme example should work
changeset
Christian Urban <urbanc@in.tum.de> [Wed, 17 Mar 2010 08:07:25 +0100] rev 1466
commented out examples that should not work; but for example type-scheme example should work
Wed, 17 Mar 2010 06:49:33 +0100 added another supp-proof for the non-recursive case
changeset
Christian Urban <urbanc@in.tum.de> [Wed, 17 Mar 2010 06:49:33 +0100] rev 1465
added another supp-proof for the non-recursive case
Tue, 16 Mar 2010 20:07:13 +0100 Revert 7c8cd6eae8e2, now all proofs in Term5 go through, both recursive and not.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 16 Mar 2010 20:07:13 +0100] rev 1464
Revert 7c8cd6eae8e2, now all proofs in Term5 go through, both recursive and not.
Tue, 16 Mar 2010 18:19:00 +0100 merge
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 16 Mar 2010 18:19:00 +0100] rev 1463
merge
Tue, 16 Mar 2010 18:18:08 +0100 The old recursive alpha works fine.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 16 Mar 2010 18:18:08 +0100] rev 1462
The old recursive alpha works fine.
Tue, 16 Mar 2010 18:13:34 +0100 added the final unfolded result
changeset
Christian Urban <urbanc@in.tum.de> [Tue, 16 Mar 2010 18:13:34 +0100] rev 1461
added the final unfolded result
Tue, 16 Mar 2010 18:02:08 +0100 merge and proof of support for non-recursive case
changeset
Christian Urban <urbanc@in.tum.de> [Tue, 16 Mar 2010 18:02:08 +0100] rev 1460
merge and proof of support for non-recursive case
Tue, 16 Mar 2010 17:20:46 +0100 Added Term5 non-recursive. The bug is there only for the recursive case.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 16 Mar 2010 17:20:46 +0100] rev 1459
Added Term5 non-recursive. The bug is there only for the recursive case.
Tue, 16 Mar 2010 17:11:32 +0100 Alpha is wrong.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 16 Mar 2010 17:11:32 +0100] rev 1458
Alpha is wrong.
Tue, 16 Mar 2010 16:51:06 +0100 alpha_bn doesn't need the permutation in non-recursive case.
changeset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 16 Mar 2010 16:51:06 +0100] rev 1457
alpha_bn doesn't need the permutation in non-recursive case.
(0) -1000 -300 -100 -60 +60 +100 +300 +1000 tip
nominal2