Hello, this example contains a function defined using Equations and a measure function. All recursive calls can be proved using the same tactic. Is there a way to tell the system I want to apply this tactic on all obligations?
There's Solve All Obligations with tactic.
However, for equivalent results, you'll need to prepend the current default obligation tactic — which Show Obligation Tactic.
should show.
You can also change Equations
to Equations?
which will allow you to prove all obligations in a single proof mode, where you can use a goal selector, eg. all: <tactics>
Last updated: Sep 25 2023 at 12:01 UTC