coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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." ?https://github.com/edwinb/Idris-dev/blob/a76627e7a62cd0816001017439523d491c4c9e8d/src/Core/TT.hs
(and if not, is there some toy project that implements a minimal verifier?)
- [Coq-Club] Core Verifier of Coq, t x, 09/08/2013
- Re: [Coq-Club] Core Verifier of Coq, Gabriel Scherer, 09/08/2013
- Re: [Coq-Club] Core Verifier of Coq, Arnaud Spiwack, 09/09/2013
- Re: [Coq-Club] Core Verifier of Coq, Enrico Tassi, 09/12/2013
- Re: [Coq-Club] Core Verifier of Coq, Gabriel Scherer, 09/08/2013
Archive powered by MHonArc 2.6.18.