Documentation

Lean.Elab.Tactic.Injection

def Lean.Elab.Tactic.evalInjection :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalInjection stx = do let fvarId ← Lean.Elab.Tactic.elabAsFVar (Lean.Syntax.getOp stx 1) none let ids : List Lean.Name := Lean.Elab.Tactic.getInjectionNewIds (Lean.Syntax.getOp stx 2) Lean.Elab.Tactic.liftMetaTactic fun mvarId => do let a ← Lean.Meta.injection mvarId fvarId ids match a with | Lean.Meta.InjectionResult.solved => do Lean.Elab.Tactic.checkUnusedIds mvarId ids pure [] | Lean.Meta.InjectionResult.subgoal mvarId' x unusedIds => do Lean.Elab.Tactic.checkUnusedIds mvarId unusedIds pure [mvarId']

def Lean.Elab.Tactic.evalInjections :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.evalInjections stx = Lean.Elab.Tactic.liftMetaTactic fun mvarId => do let a ← Lean.Meta.injections mvarId 5 match a with | none => pure [] | some mvarId => pure [mvarId]