- 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.

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

.

## Instances For

## Equations

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

## 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]

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 any of the selected tactic applications fail, it will call `failed`

with the main goal mvar.

## Equations

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