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: Apr 14 2024 at 11:02 UTC