The Coq mailing list

[Andrew Pennebaker <andrew.pennebaker AT gmail.com>]

Daniel, I'll check it out.

Adam, I started reading CPDT Chapter 3 and came up with this:

https://github.com/mcandre/mcandre/blob/master/coq/bertrand.v

Cheers,

Andrew Pennebaker

www.yellosoft.us

On Wed, Nov 2, 2011 at 7:49 PM, Daniel Schepler <dschepler AT gmail.com> wrote:

I've started working on a Coq tutorial focused more on mathematics formalization than on program verification.  Right now, I only have the first chapter done, without even an introduction written (although I have a rough outline in mind for what I want to cover -- it hopefully shouldn't be too hard to find in the recent coq-club archives).

This first chapter starts off by declaring the "language/syntax" of the theory of groups, then declaring the "axioms", then proving several basic results using the axioms.

I'd be interested in any comments you might have about it.
--
Daniel Schepler