Denotes a set of locations where a tactic should be applied for the main goal. See also `withLocation`

.

- wildcard: Lean.Elab.Tactic.Location
Apply the tactic everywhere.

- targets: Array Lean.Syntax → Bool → Lean.Elab.Tactic.Location
`hypotheses`

are hypothesis names in the main goal that the tactic should be applied to. If`type`

is true, then the tactic should also be applied to the target type.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- Lean.Elab.Tactic.expandOptLocation stx = if Lean.Syntax.isNone stx = true then Lean.Elab.Tactic.Location.targets #[] true else Lean.Elab.Tactic.expandLocation stx[0]

## Instances For

def
Lean.Elab.Tactic.withLocation
(loc : Lean.Elab.Tactic.Location)
(atLocal : Lean.FVarId → Lean.Elab.Tactic.TacticM Unit)
(atTarget : Lean.Elab.Tactic.TacticM Unit)
(failed : Lean.MVarId → Lean.Elab.Tactic.TacticM Unit)
:

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 target first and then the hypotheses in reverse order. If`atTarget`

closes the main goal,`withLocation`

does not run`atLocal`

. If all tactic applications fail,`withLocation`

with call`failed`

with the main goal mvar.

## Equations

- One or more equations did not get rendered due to their size.