| Sun, 16 Nov 2008 15:04:21 -0500 |
Adam Chlipala |
About to stop using JMeq |
| Sun, 16 Nov 2008 14:01:33 -0500 |
Adam Chlipala |
Closure conversion defined |
| Mon, 10 Nov 2008 14:12:22 -0500 |
Adam Chlipala |
PatMatch Elaborate_correct |
| Mon, 10 Nov 2008 11:36:00 -0500 |
Adam Chlipala |
CpsExp_correct |
| Sun, 09 Nov 2008 15:15:41 -0500 |
Adam Chlipala |
System F |
| Mon, 03 Nov 2008 14:47:46 -0500 |
Adam Chlipala |
Interderivability of big and small step |
| Sat, 18 Oct 2008 12:04:28 -0400 |
Adam Chlipala |
Up to Streicher |
| Wed, 08 Oct 2008 09:41:50 -0400 |
Adam Chlipala |
crush' pursues trivial inversions |
| Tue, 07 Oct 2008 10:43:54 -0400 |
Adam Chlipala |
Get Coinductive compiling again |
| Mon, 06 Oct 2008 14:33:11 -0400 |
Adam Chlipala |
Start of certified regexp matcher |
| Mon, 06 Oct 2008 13:07:24 -0400 |
Adam Chlipala |
Tagless interpreter & cfold |
| Sun, 05 Oct 2008 20:07:35 -0400 |
Adam Chlipala |
Incorporate crush' bug reports; ilists in MoreDep |
| Sat, 04 Oct 2008 14:58:00 -0400 |
Adam Chlipala |
Try arithmetic contradiction |
| Wed, 01 Oct 2008 09:33:44 -0400 |
Adam Chlipala |
Put [try] in front of [subst], to avoid whining about recursive equalities |
| Wed, 01 Oct 2008 09:32:36 -0400 |
Adam Chlipala |
Remove [done] markers after enhancement phase finishes |
| Tue, 30 Sep 2008 17:47:59 -0400 |
Adam Chlipala |
Co-inductive evaluation example |
| Tue, 30 Sep 2008 13:11:39 -0400 |
Adam Chlipala |
Beefed-up crush, with auto-inversion and lemma instantiation |
| Sun, 28 Sep 2008 12:44:05 -0400 |
Adam Chlipala |
What could go wrong; some exercises |
| Sun, 28 Sep 2008 11:57:15 -0400 |
Adam Chlipala |
Recursive predicates |
| Fri, 12 Sep 2008 16:55:37 -0400 |
Adam Chlipala |
Exercises |
| Wed, 10 Sep 2008 15:47:22 -0400 |
Adam Chlipala |
Nested Inductive Types |
| Wed, 03 Sep 2008 13:30:05 -0400 |
Adam Chlipala |
Squash book into main directory
base
book/src/Tactics.v@0f4beab7a783
|
