inductive Lean.Elab.Tactic.Location : Type

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 (hypotheses : Array Lean.Syntax) (type : 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.

def Lean.Elab.Tactic.expandLocation (stx : Lean.Syntax) : Lean.Elab.Tactic.Location

Equations

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

def Lean.Elab.Tactic.expandOptLocation (stx : Lean.Syntax) : Lean.Elab.Tactic.Location

Equations

• Lean.Elab.Tactic.expandOptLocation stx = if stx.isNone = 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) : 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.