Optional tactics

Stream: Is there code for X?

[Mr Proof]

Say I have a proof like:

def myProof:propType := by A;B;C;D;E

Where A,B,C,D are the tactics. If I have an extra "simp" tactic that doesn't simplify anything I don't want this to fail.

If a tactic fails to achieve any new goals I think it should just show a warning message and carry on to the next tactic.

Are there any settings of code such as try{tactic} that would facilitate that?

Why?

For example if I had a set of tactics A;B;C;D;E that work on a lot of proofs when put in that order. Except in some proofs C is unnecessary then why should it cause an error?

[Eric Wieser]

try tactic should work

[Mr Proof]

It does!