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?
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: Feb 06 2023 at 12:04 UTC