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: Jan 29 2023 at 03:28 UTC