Stream: Coq users

Topic: External type checker for Coq

view this post on Zulip Roman Bars (Mar 27 2021 at 07:43):

Lean can export fully elaborated proof terms and there are external type checkers for those terms. Is there something similar for Coq?

view this post on Zulip Guillaume Melquiond (Mar 27 2021 at 07:48):

Kind of. There is no separate file format, since .vo already contains the elaborated proof terms. And the program is called coqchk. It is a smaller version of Coq's kernel.

Last updated: Sep 30 2023 at 06:01 UTC