Lean.Meta.Tactic.Replace

Equations

Lean.Meta.replaceTargetEq mvarId targetNew eqProof = Lean.Meta.withMVarContext mvarId do Lean.Meta.checkNotAssigned mvarId `replaceTarget let tag ← Lean.Meta.getMVarTag mvarId let mvarNew ← Lean.Meta.mkFreshExprSyntheticOpaqueMVar targetNew tag let target ← Lean.Meta.getMVarType mvarId let u ← Lean.Meta.getLevel target let eq ← Lean.Meta.mkEq target targetNew let _ ← Lean.Meta.mkExpectedTypeHint eqProof eq let val : Lean.Expr := Lean.mkAppN (Lean.mkConst `Eq.mpr [u]) #[target, targetNew, eqProof, mvarNew] Lean.Meta.assignExprMVar mvarId val pure (Lean.Expr.mvarId! mvarNew)

Equations

Equations

Lean.Meta.replaceLocalDecl mvarId fvarId typeNew eqProof = (fun findMaxFVar => Lean.Meta.withMVarContext mvarId do let localDecl ← Lean.Meta.getLocalDecl fvarId let typeNewPr ← Lean.Meta.mkEqMP eqProof (Lean.mkFVar fvarId) let discr ← StateRefT'.run (findMaxFVar typeNew) localDecl let x : Unit × Lean.LocalDecl := discr match x with | (x, localDecl') => do let result ← Lean.Meta.assertAfter mvarId (Lean.LocalDecl.fvarId localDecl') (Lean.LocalDecl.userName localDecl) typeNew typeNewPr HOrElse.hOrElse (do let mvarIdNew ← Lean.Meta.clear result.mvarId fvarId pure { fvarId := result.fvarId, mvarId := mvarIdNew, subst := result.subst }) fun x => pure result) Lean.Meta.replaceLocalDecl.findMaxFVar

Equations

Equations

Lean.Meta.replaceLocalDeclDefEq mvarId fvarId typeNew = Lean.Meta.withMVarContext mvarId do let mvarDecl ← Lean.Meta.getMVarDecl mvarId if (typeNew == mvarDecl.type) = true then pure mvarId else do let a ← Lean.getLCtx let lctxNew : Lean.LocalContext := Lean.LocalContext.modifyLocalDecl a fvarId fun a => Lean.LocalDecl.setType a typeNew let a ← Lean.Meta.getLocalInstances let mvarNew ← Lean.Meta.mkFreshExprMVarAt lctxNew a mvarDecl.type mvarDecl.kind mvarDecl.userName 0 Lean.Meta.assignExprMVar mvarId mvarNew pure (Lean.Expr.mvarId! mvarNew)

def Lean.Meta.change (mvarId : Lean.MVarId) (targetNew : Lean.Expr) (checkDefEq : optParam Bool true) :

Equations

Lean.Meta.change mvarId targetNew checkDefEq = Lean.Meta.withMVarContext mvarId do let target ← Lean.Meta.getMVarType mvarId let _do_jp : PUnit → Lean.MetaM Lean.MVarId := fun y => Lean.Meta.replaceTargetDefEq mvarId targetNew if checkDefEq = true then do let a ← Lean.Meta.isDefEq target targetNew if a = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.Meta.throwTacticEx `change mvarId (Lean.toMessageData "given type" ++ Lean.toMessageData (Lean.indentExpr targetNew) ++ Lean.toMessageData "\nis not definitionally equal to" ++ Lean.toMessageData (Lean.indentExpr target) ++ Lean.toMessageData "") Lean.Syntax.missing _do_jp y else do let y ← pure PUnit.unit _do_jp y

Equations

Lean.Meta.changeLocalDecl mvarId fvarId typeNew checkDefEq = do Lean.Meta.checkNotAssigned mvarId `changeLocalDecl let discr ← Lean.Meta.revert mvarId #[fvarId] true let x : Array Lean.FVarId × Lean.MVarId := discr match x with | (xs, mvarId) => Lean.Meta.withMVarContext mvarId (let numReverted := Array.size xs; do let target ← Lean.Meta.getMVarType mvarId let check : Lean.Expr → Lean.MetaM Unit := fun typeOld => if checkDefEq = true then do let a ← Lean.Meta.isDefEq typeNew typeOld if a = true then pure PUnit.unit else Lean.Meta.throwTacticEx `changeHypothesis mvarId (Lean.toMessageData "given type" ++ Lean.toMessageData (Lean.indentExpr typeNew) ++ Lean.toMessageData "\nis not definitionally equal to" ++ Lean.toMessageData (Lean.indentExpr typeOld) ++ Lean.toMessageData "") Lean.Syntax.missing else pure PUnit.unit let finalize : Lean.Expr → Lean.MetaM Lean.MVarId := fun targetNew => do let mvarId ← Lean.Meta.replaceTargetDefEq mvarId targetNew let discr ← Lean.Meta.introNP mvarId numReverted let x : Array Lean.FVarId × Lean.MVarId := discr match x with | (x, mvarId) => pure mvarId match target with | Lean.Expr.forallE n d b c => do check d finalize (Lean.mkForall n (Lean.Expr.Data.binderInfo c) typeNew b) | Lean.Expr.letE n t v b x => do check t finalize (Lean.mkLet n typeNew v b) | x => Lean.Meta.throwTacticEx `changeHypothesis mvarId (Function.comp Lean.MessageData.ofFormat Lean.format "unexpected auxiliary target") Lean.Syntax.missing)

Equations

Equations