Stream: MetaCoq

Topic: squashing in infer_template_program?

view this post on Zulip 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.)

view this post on Zulip Théo Winterhalter (Nov 04 2022 at 06:30):

I think it's so erasure will remove the proof part.

Last updated: Feb 04 2023 at 02:03 UTC