inductive Lean.Elab.Tactic.Location : Type

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

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