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?
Yes, have a look at Proof.run_tactic.
Last updated: Jan 29 2023 at 03:28 UTC