The Coq mailing list

[t x <txrev319 AT gmail.com>]

As a followup to this thread:
https://sympa.inria.fr/sympa/arc/coq-club/2013-05/msg00071.html

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!