Sun, 02 Nov 2008 13:14:08 -0500 |
Adam Chlipala |
Progress and preservation |
Sun, 02 Nov 2008 12:20:56 -0500 |
Adam Chlipala |
Fix some uglyness |
Sun, 02 Nov 2008 12:16:55 -0500 |
Adam Chlipala |
Proved concrete substitution |
Wed, 29 Oct 2008 17:50:09 -0400 |
Adam Chlipala |
a -> an |
Wed, 29 Oct 2008 17:41:38 -0400 |
Adam Chlipala |
Reflection exercise |
Wed, 29 Oct 2008 14:39:00 -0400 |
Adam Chlipala |
Reflection exercise |
Tue, 28 Oct 2008 17:03:25 -0400 |
Adam Chlipala |
Templatize Reflection |
Tue, 28 Oct 2008 16:31:55 -0400 |
Adam Chlipala |
my_tauto prose |
Tue, 28 Oct 2008 15:50:44 -0400 |
Adam Chlipala |
monoid prose |
Tue, 28 Oct 2008 15:28:52 -0400 |
Adam Chlipala |
Monoid code |
Tue, 28 Oct 2008 14:28:22 -0400 |
Adam Chlipala |
Code for my_tauto |
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 |
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 |
Sun, 12 Oct 2008 08:44:23 -0400 |
Adam Chlipala |
s/stream/tree |
Wed, 08 Oct 2008 14:22:47 -0400 |
Adam Chlipala |
Fix red-black section heading |
Wed, 08 Oct 2008 14:18:35 -0400 |
Adam Chlipala |
Add a darn newline |
Wed, 08 Oct 2008 13:55:20 -0400 |
Adam Chlipala |
Exercise added at end of MoreDep |
Wed, 08 Oct 2008 10:01:26 -0400 |
Adam Chlipala |
Templatize MoreDep |
Wed, 08 Oct 2008 09:41:50 -0400 |
Adam Chlipala |
crush' pursues trivial inversions |