| Tue, 28 Oct 2008 13:19:33 -0400 |
Adam Chlipala |
Trivial tautologies |
| Tue, 28 Oct 2008 11:29:14 -0400 |
Adam Chlipala |
Start of Reflection |
| Mon, 27 Oct 2008 10:31:57 -0400 |
Adam Chlipala |
Templatize Match |
| Mon, 27 Oct 2008 10:09:10 -0400 |
Adam Chlipala |
Prose for matcher |
| Sun, 26 Oct 2008 17:10:20 -0400 |
Adam Chlipala |
inster example |
| Sun, 26 Oct 2008 16:45:19 -0400 |
Adam Chlipala |
Uncommented matcher code |
| Sun, 26 Oct 2008 15:18:13 -0400 |
Adam Chlipala |
Functional programming in Ltac |
| Sun, 26 Oct 2008 14:39:21 -0400 |
Adam Chlipala |
Free variables in unification variables issue |
| Sun, 26 Oct 2008 14:11:41 -0400 |
Adam Chlipala |
Through completer' |
| Sun, 26 Oct 2008 11:13:43 -0400 |
Adam Chlipala |
autorewrite |
| Sun, 26 Oct 2008 10:28:00 -0400 |
Adam Chlipala |
auto |
| Wed, 22 Oct 2008 14:32:41 -0400 |
Adam Chlipala |
Start of Match |
| Wed, 22 Oct 2008 13:40:32 -0400 |
Adam Chlipala |
call-by-name is really call-by-need |
| Wed, 22 Oct 2008 09:43:37 -0400 |
Adam Chlipala |
Clarify intent to use hlist |
| Wed, 22 Oct 2008 07:50:47 -0400 |
Adam Chlipala |
s/reflexive/index function |
| Mon, 20 Oct 2008 17:02:04 -0400 |
Adam Chlipala |
s/itree/htree |
| Mon, 20 Oct 2008 14:03:08 -0400 |
Adam Chlipala |
Equality exercise |
| Mon, 20 Oct 2008 12:17:39 -0400 |
Adam Chlipala |
More DepList notations |
| Mon, 20 Oct 2008 10:44:20 -0400 |
Adam Chlipala |
Add ext_eq axiom and DepList notations |
| Mon, 20 Oct 2008 09:11:54 -0400 |
Adam Chlipala |
Templatize Equality |
| Sat, 18 Oct 2008 17:36:08 -0400 |
Adam Chlipala |
ext_eq |
| Sat, 18 Oct 2008 15:32:59 -0400 |
Adam Chlipala |
Definitional equality |
| Sat, 18 Oct 2008 14:55:52 -0400 |
Adam Chlipala |
Interconvertibility |
| Sat, 18 Oct 2008 14:24:11 -0400 |
Adam Chlipala |
JMeq |
