The Coq mailing list

[Jonas Oberhauser <s9joober AT gmail.com>]

Am 18.05.2013 03:29, schrieb Math Prover:

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!
Hi Math prover,

You should check the book Coq'Art, which I recall gives a very nice explanation of the theoretical framework of Coq.

Kind regards, Jonas