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 |
Sat, 18 Oct 2008 13:52:09 -0400 |
Adam Chlipala |
Proofs with equality |
Sat, 18 Oct 2008 12:04:28 -0400 |
Adam Chlipala |
Up to Streicher |
Tue, 14 Oct 2008 15:21:02 -0400 |
Adam Chlipala |
Clarify exercise wording |
Tue, 14 Oct 2008 15:11:14 -0400 |
Adam Chlipala |
Pattern-matching exercise |
Tue, 14 Oct 2008 14:58:33 -0400 |
Adam Chlipala |
itree exercise |
Tue, 14 Oct 2008 14:49:51 -0400 |
Adam Chlipala |
DepList |
Tue, 14 Oct 2008 13:05:43 -0400 |
Adam Chlipala |
Templatize DataStruct |
Tue, 14 Oct 2008 11:28:44 -0400 |
Adam Chlipala |
Commentary on cond example |
Tue, 14 Oct 2008 10:52:38 -0400 |
Adam Chlipala |
Code for cond-folding example |
Mon, 13 Oct 2008 15:09:58 -0400 |
Adam Chlipala |
Index functions |
Mon, 13 Oct 2008 14:04:39 -0400 |
Adam Chlipala |
Recursive type definitions |
Mon, 13 Oct 2008 13:20:57 -0400 |
Adam Chlipala |
STLC interp |
Mon, 13 Oct 2008 12:35:48 -0400 |
Adam Chlipala |
hlist and hget |
Mon, 13 Oct 2008 11:59:20 -0400 |
Adam Chlipala |
Commentary on ilist get |
Mon, 13 Oct 2008 10:47:21 -0400 |
Adam Chlipala |
Start of DataStruct |