camp coq update

Ian Lynagh igloo at
Wed Apr 1 14:18:26 EDT 2009

Hi all,

Camp coq update:

Florent Becker and I are converging on the way to structure coq proofs,
the datatypes, etc. I've also interleaved the coq definitions, proofs
etc with the LaTeX paper, in
    darcs get
The .v files are understood directly by coq, while running "make" turns
them into .tex file that latex understands, with the coq displayed in
green boxes.

Many of the easier proofs, lifting {axioms on unnamed patches} into
{lemmas on named patches}, are done.

Starting on the more meaty proofs, I'm currently stuck on the "Foo"
sub-lemma, heading towards Lemma 10.1 (commute-in-sequence-consistent).
I think it should be quite easy once I work out the trick.


More information about the Camp mailing list