Equations
- Lean.Elab.Tactic.deltaLocalDecl declName fvarId = do let mvarId ← Lean.Elab.Tactic.getMainGoal let localDecl ← liftM (Lean.Meta.getLocalDecl fvarId) let typeNew ← liftM (Lean.Meta.deltaExpand (Lean.LocalDecl.type localDecl) fun a => a == declName) let _do_jp : PUnit → Lean.Elab.Tactic.TacticM Unit := fun y => do let a ← liftM (Lean.Meta.replaceLocalDeclDefEq mvarId fvarId typeNew) Lean.Elab.Tactic.replaceMainGoal [a] if (typeNew == Lean.LocalDecl.type localDecl) = true then do let y ← liftM (Lean.Meta.throwTacticEx `delta mvarId (Lean.toMessageData "did not delta reduce '" ++ Lean.toMessageData declName ++ Lean.toMessageData "' at '" ++ Lean.toMessageData (Lean.LocalDecl.userName localDecl) ++ Lean.toMessageData "'") Lean.Syntax.missing) _do_jp y else do let y ← pure PUnit.unit _do_jp y
Equations
- Lean.Elab.Tactic.deltaTarget declName = do let mvarId ← Lean.Elab.Tactic.getMainGoal let target ← Lean.Elab.Tactic.getMainTarget let targetNew ← liftM (Lean.Meta.deltaExpand target fun a => a == declName) let _do_jp : PUnit → Lean.Elab.Tactic.TacticM Unit := fun y => do let a ← liftM (Lean.Meta.replaceTargetDefEq mvarId targetNew) Lean.Elab.Tactic.replaceMainGoal [a] if (targetNew == target) = true then do let y ← liftM (Lean.Meta.throwTacticEx `delta mvarId (Lean.toMessageData "did not delta reduce '" ++ Lean.toMessageData declName ++ Lean.toMessageData "'") Lean.Syntax.missing) _do_jp y else do let y ← pure PUnit.unit _do_jp y
Equations
- Lean.Elab.Tactic.evalDelta stx = do let declName ← Lean.resolveGlobalConstNoOverload (Lean.Syntax.getOp stx 1) let loc : Lean.Elab.Tactic.Location := Lean.Elab.Tactic.expandOptLocation (Lean.Syntax.getOp stx 2) Lean.Elab.Tactic.withLocation loc (Lean.Elab.Tactic.deltaLocalDecl declName) (Lean.Elab.Tactic.deltaTarget declName) fun a => liftM (Lean.Meta.throwTacticEx `delta a (Lean.toMessageData "did not delta reduce '" ++ Lean.toMessageData declName ++ Lean.toMessageData "'") Lean.Syntax.missing)