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: May 28 2023 at 18:29 UTC