I’m writing a plugin that suggests a sequence of tactics to copy-and-paste into my proof.
I would prefer not to generate tactics that fail. My idea is to first build the Proofview
representation of these tactics, and then to silently “execute them” on a goal/environment. If it fails, my plugin is to consider different tactics.
Is this possible?