# Documentation

Lean.Elab.Tactic.Location

• Apply the tactic everywhere.

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

targets:

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
• = if then else
def Lean.Elab.Tactic.withLocation (loc : Lean.Elab.Tactic.Location) (atLocal : ) (atTarget : ) (failed : ) :

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.