Jason Gross (Nov 03 2022 at 17:47): Jason Gross (Nov 03 2022 at 17:47):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.)
Théo Winterhalter (Nov 04 2022 at 06:30):I think it's so erasure will remove the proof part.
Last updated: Apr 20 2024 at 15:01 UTC