Why does MetaCoq.SafeChecker.SafeTemplateChecker.infer_template_program return squashed proofs? (I'm trying to use it to get proofs of a bunch of things.)
MetaCoq.SafeChecker.SafeTemplateChecker.infer_template_program
I think it's so erasure will remove the proof part.
Last updated: Feb 04 2023 at 02:03 UTC