log

age author description
Tue, 04 Nov 2008 12:39:28 -0500 Adam Chlipala Evaluation contexts ahoy
Tue, 04 Nov 2008 11:23:20 -0500 Adam Chlipala Firstorder clean-ups after class
Mon, 03 Nov 2008 14:47:46 -0500 Adam Chlipala Interderivability of big and small step
Mon, 03 Nov 2008 09:50:22 -0500 Adam Chlipala Add Plus
Mon, 03 Nov 2008 09:43:32 -0500 Adam Chlipala Hoas, up to type soundness
Sun, 02 Nov 2008 14:41:01 -0500 Adam Chlipala Simplify Concrete
Sun, 02 Nov 2008 13:51:51 -0500 Adam Chlipala De Bruijn
Sun, 02 Nov 2008 13:25:42 -0500 Adam Chlipala Removed G2 everywhere
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