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 https://github.com/leanprover/lean/blob/master/doc/export_format.md 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