- wildcard: Lean.Elab.Tactic.Location
- targets: Array Lean.Syntax → Bool → Lean.Elab.Tactic.Location
Equations
- Lean.Elab.Tactic.expandLocation stx = let arg := Lean.Syntax.getOp stx 1; if (Lean.Syntax.getKind arg == `Lean.Parser.Tactic.locationWildcard) = true then Lean.Elab.Tactic.Location.wildcard else Lean.Elab.Tactic.Location.targets (Lean.Syntax.getArgs (Lean.Syntax.getOp arg 0)) !Lean.Syntax.isNone (Lean.Syntax.getOp arg 1)
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)
:
Equations
- Lean.Elab.Tactic.withLocation loc atLocal atTarget failed = match loc with | Lean.Elab.Tactic.Location.targets hyps type => do Array.forM (fun hyp => Lean.Elab.Tactic.withMainContext do let fvarId ← Lean.Elab.Tactic.getFVarId hyp atLocal fvarId) hyps 0 (Array.size hyps) if type = true then atTarget else pure PUnit.unit | Lean.Elab.Tactic.Location.wildcard => do let worked ← Lean.Elab.Tactic.tryTactic (Lean.Elab.Tactic.withMainContext atTarget) Lean.Elab.Tactic.withMainContext (let worked := worked; do let a ← Lean.getLCtx let r ← let col := Array.reverse (Lean.LocalContext.getFVarIds a); forIn col worked fun fvarId r => let worked := r; do let a ← Lean.Elab.Tactic.tryTactic (Lean.Elab.Tactic.withMainContext (atLocal fvarId)) let worked : Bool := worked || a pure PUnit.unit pure (ForInStep.yield worked) let x : Bool := r let worked : Bool := x if worked = true then pure PUnit.unit else do let a ← Lean.Elab.Tactic.getMainGoal failed a)