Documentation

Lean.Elab.Tactic.Location

inductive Lean.Elab.Tactic.Location:

Type

wildcard: Lean.Elab.Tactic.Location
targets: Array Lean.Syntax → Bool → Lean.Elab.Tactic.Location

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 (Lean.Syntax.getOp 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

Equations

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