| Sun, 22 Apr 2012 15:51:03 -0400 |
Adam Chlipala |
Citations for continuations and unification |
| Sun, 22 Apr 2012 15:38:11 -0400 |
Adam Chlipala |
Define 'certified program' |
| Fri, 20 Apr 2012 12:49:47 -0400 |
Adam Chlipala |
Typo fixes |
| Thu, 12 Apr 2012 18:46:55 -0400 |
Adam Chlipala |
Typo fix |
| Thu, 12 Apr 2012 18:45:48 -0400 |
Adam Chlipala |
New release |
| Thu, 12 Apr 2012 18:41:32 -0400 |
Adam Chlipala |
Comment CpdtTactics.v |
| Thu, 12 Apr 2012 16:27:28 -0400 |
Adam Chlipala |
Baffling unification messages explained |
| Thu, 12 Apr 2012 15:54:37 -0400 |
Adam Chlipala |
A pass over Large |
| Thu, 12 Apr 2012 14:30:53 -0400 |
Adam Chlipala |
A pass through Match |
| Thu, 12 Apr 2012 12:11:29 -0400 |
Adam Chlipala |
More discussion of axiom avoidance and tactic pitfalls for JMeq |
| Sun, 08 Apr 2012 11:11:27 -0400 |
Adam Chlipala |
Strengthen last theorem of Coinductive |
| Tue, 03 Apr 2012 15:10:04 -0400 |
Adam Chlipala |
Conclusion |
| Sun, 01 Apr 2012 15:14:44 -0400 |
Adam Chlipala |
Typo fixes |
| Sun, 01 Apr 2012 15:02:32 -0400 |
Adam Chlipala |
New chapter: ProgLang |
| Thu, 29 Mar 2012 18:10:52 -0400 |
Adam Chlipala |
Get it to build with Coq 8.4 |
| Thu, 29 Mar 2012 17:15:14 -0400 |
Adam Chlipala |
Date increment |
| Thu, 29 Mar 2012 17:13:23 -0400 |
Adam Chlipala |
Recursing under binders in reification |
| Wed, 28 Mar 2012 13:20:50 -0400 |
Adam Chlipala |
One more example of avoiding axioms (getNat) |
| Mon, 26 Mar 2012 17:00:34 -0400 |
Adam Chlipala |
New release |
| Mon, 26 Mar 2012 16:55:59 -0400 |
Adam Chlipala |
Finish pass over LogicProg; change [crush] to take advantage of new [Hint Rewrite] syntax that uses database [core] by default |
| Mon, 26 Mar 2012 16:24:19 -0400 |
Adam Chlipala |
Prose for third LogicProg section |
| Mon, 26 Mar 2012 16:04:52 -0400 |
Adam Chlipala |
Prose for second LogicProg section |
| Mon, 26 Mar 2012 15:35:09 -0400 |
Adam Chlipala |
Prose for first LogicProg section |
| Fri, 02 Mar 2012 10:52:22 -0500 |
Adam Chlipala |
The one rule of dependent pattern matching |
| Fri, 02 Mar 2012 09:58:00 -0500 |
Adam Chlipala |
Move exercises out of mainline book |
| Fri, 16 Dec 2011 13:28:11 -0500 |
Adam Chlipala |
Change make invocations to work properly with -j |
| Wed, 09 Nov 2011 15:26:50 -0500 |
Adam Chlipala |
Templatize Large |
| Tue, 08 Nov 2011 11:54:09 -0500 |
Adam Chlipala |
Pass over old Large material; index fixes |
| Sun, 06 Nov 2011 16:54:40 -0500 |
Adam Chlipala |
Remove home page reference to Part IV |
| Sun, 06 Nov 2011 16:52:15 -0500 |
Adam Chlipala |
Discuss reduction of [fix] |
| Sun, 06 Nov 2011 16:25:45 -0500 |
Adam Chlipala |
Pass through old content of Equality |
| Thu, 03 Nov 2011 17:04:41 -0400 |
Adam Chlipala |
Explicit note about primitive recursion restriction, early on |
| Wed, 02 Nov 2011 17:03:25 -0400 |
Adam Chlipala |
Template tweaks |
| Wed, 02 Nov 2011 16:22:41 -0400 |
Adam Chlipala |
New subsection on Ltac reification |
| Wed, 02 Nov 2011 14:48:25 -0400 |
Adam Chlipala |
Pass through old content of Reflection |
| Tue, 01 Nov 2011 12:34:00 -0400 |
Adam Chlipala |
Tweak Generic templating |
| Mon, 31 Oct 2011 14:24:16 -0400 |
Adam Chlipala |
Pass over Generic |
| Fri, 28 Oct 2011 18:26:16 -0400 |
Adam Chlipala |
New release |
| Fri, 28 Oct 2011 17:43:53 -0400 |
Adam Chlipala |
First draft of full prose for GeneralRec |
| Fri, 28 Oct 2011 15:38:41 -0400 |
Adam Chlipala |
Prose for domain-theoretic approach |
| Wed, 26 Oct 2011 18:37:47 -0400 |
Adam Chlipala |
Co-inductive non-termination monads |
| Wed, 26 Oct 2011 17:14:28 -0400 |
Adam Chlipala |
Move GeneralRec one chapter slot later, since Subset should be a prereq |
| Wed, 26 Oct 2011 16:57:11 -0400 |
Adam Chlipala |
Non-termination monad |
| Wed, 26 Oct 2011 15:12:21 -0400 |
Adam Chlipala |
Well-founded recursion |
| Wed, 26 Oct 2011 11:19:52 -0400 |
Adam Chlipala |
Stub out new chapter |
| Tue, 25 Oct 2011 10:56:00 -0400 |
Adam Chlipala |
Fix template |
| Tue, 25 Oct 2011 10:51:31 -0400 |
Adam Chlipala |
Typo fix in template comment |
| Sun, 23 Oct 2011 14:48:52 -0400 |
Adam Chlipala |
Finished pass over Coinductive |
| Sun, 23 Oct 2011 13:33:46 -0400 |
Adam Chlipala |
Pass through Coinductive up to PL example |
| Wed, 19 Oct 2011 10:00:07 -0400 |
Adam Chlipala |
One more axiom avoidance example |
| Mon, 17 Oct 2011 14:56:46 -0400 |
Adam Chlipala |
New section on avoiding axioms |
| Mon, 17 Oct 2011 11:09:23 -0400 |
Adam Chlipala |
Pass over Universes |
| Sun, 16 Oct 2011 10:46:15 -0400 |
Adam Chlipala |
Pass through DataStruct |
| Sun, 16 Oct 2011 08:54:36 -0400 |
Adam Chlipala |
Typo fix |
| Thu, 13 Oct 2011 10:24:39 -0400 |
Adam Chlipala |
More coqdoc bug workarounds |
| Mon, 10 Oct 2011 16:12:04 -0400 |
Adam Chlipala |
Work around coqdoc bug |
| Mon, 10 Oct 2011 16:01:31 -0400 |
Adam Chlipala |
Pass over MoreDep |
| Thu, 06 Oct 2011 12:04:55 -0400 |
Adam Chlipala |
Hide some more Subset code in template |
| Wed, 05 Oct 2011 11:33:30 -0400 |
Adam Chlipala |
New release |
| Wed, 05 Oct 2011 11:32:13 -0400 |
Adam Chlipala |
Pass over Subset |
| Tue, 04 Oct 2011 13:38:21 -0400 |
Adam Chlipala |
Change some template annotations |
| Mon, 03 Oct 2011 11:19:12 -0400 |
Adam Chlipala |
New release |
| Mon, 03 Oct 2011 11:15:51 -0400 |
Adam Chlipala |
Remove Part IV |
| Sun, 02 Oct 2011 16:34:15 -0400 |
Adam Chlipala |
Finish adding Match exercises |
