Lean4
/-- Runs the given `atLocal` and `atTarget` methods on each of the locations selected by the given
`loc`.
* If `loc` is a list of locations, runs at each specified hypothesis (and finally the goal if `⊢` is
included), and fails if any of the tactic applications fail.
* If `loc` is `*`, runs at the nondependent `Prop` hypotheses (those produced by
`Lean.MVarId.getNondepPropHyps`) and then at the target.
This is a variant of `Lean.Elab.Tactic.withLocation`. -/
def withNondepPropLocation (loc : Location) (atLocal : FVarId → TacticM Unit) (atTarget : TacticM Unit)
(failed : MVarId → TacticM Unit) : TacticM Unit := do
match loc with
| Location.targets hyps target =>
do
(← getFVarIds hyps).forM atLocal
if target then
atTarget
| Location.wildcard =>
do
let mut worked := false
for hyp in ← (← getMainGoal).getNondepPropHyps do
worked := worked || (← tryTactic <| atLocal hyp)
unless worked || (← tryTactic atTarget) do
failed (← getMainGoal)
