Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Core Verifier of Coq

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Core Verifier of Coq


Chronological Thread 
  • From: t x <txrev319 AT gmail.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: [Coq-Club] Core Verifier of Coq
  • Date: Sun, 8 Sep 2013 11:31:53 +0000

I recently installed the Idris language, and was pleasantly surprised to find that it's core verifier is only 1000 LOC:
https://github.com/edwinb/Idris-dev/blob/a76627e7a62cd0816001017439523d491c4c9e8d/src/Core/TT.hs

In Coq, is there is a corresponding *.ml file that does the checking when I type in "Qed." ?
(and if not, is there some toy project that implements a minimal verifier?)

I'm not looking for unification / inference / notation / ltac. Nor am I interested in various proofs -- just the very core "dumb/minimal" verifier that verifiers the terms generated.

Thanks!



Archive powered by MHonArc 2.6.18.

Top of Page