Try multiple tactics but use none

Stream: general

[nrs]

Is there a tactic that will try multiple tactics, print the result if it succeeds, but won't apply the tactic to the proof state? So e.g. saidTactic [apply f, simp +bool, apply g, simp, ...] will try all of these tactics on the current proof state and print only the proof states that are one tactic usage away from the current one, so I can compare which of them would be interesting to investigate next.

[Kim Morrison]

You might like to look at the implementation of hint.

[nrs]

Thank you for the suggestion!