The Coq mailing list

[Math Prover <mathprover AT yahoo.com>]

Hi Coq-Club,

  With apologies for my ignorance, can someone point me at the documentation for the core verifier of Coq?

  I've played with Coq for a few months now -- working through parts of Pierce's Software Foundations and Chlipala's CPDT, however despite proving some non-trivial theorems, I often feel that I don't understand "what's going on under the hood."

  What I'm looking for is the equivalent of

  * SICP's meta circular evaluator or

  * the epsilon-delta definition of derivatives

  If we view a 'state' as

  pair<list<hypothesis>, goal>

  Then there should be a minimal set of rules for deriving new 'states.'

  I'm looking for the minimal set of rules on top of which all valid proofs are built.

Thanks!