Roman Bars (Mar 27 2021 at 07:43): 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?
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: Oct 13 2024 at 01:02 UTC