Stream: Coq users

Topic: “Running” Proofview.tactic to see if it would succeed

view this post on Zulip RanDair Scott Porter (Aug 10 2020 at 21:30):

Suppose I have an environment, a goal term, and a Proofview.tactic. I would like my plugin to silently "execute" these tactics on the given goal/environment to be able to determine (yes/no) if it proves the goal. Is this possible?

view this post on Zulip Pierre-Marie Pédrot (Aug 10 2020 at 22:43):

Yes, have a look at Proof.run_tactic.

Last updated: Oct 13 2024 at 01:02 UTC