Lean.Meta.Tactic.Replace

def Lean.Meta.replaceTargetEq (mvarId : Lean.MVarId) (targetNew : Lean.Expr) (eqProof : Lean.Expr) :

Convert the given goal Ctx |- target into Ctx |- targetNew using an equality proof eqProof : target = targetNew. It assumes eqProof has type target = targetNew

Equations

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

source

def Lean.Meta.replaceTargetDefEq (mvarId : Lean.MVarId) (targetNew : Lean.Expr) :

Lean.MetaM Lean.MVarId

Convert the given goal Ctx | target into Ctx |- targetNew. It assumes the goals are definitionally equal. We use the proof term

@id target mvarNew

to create a checkpoint.

Equations

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

source

def Lean.Meta.replaceLocalDecl (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (typeNew : Lean.Expr) (eqProof : Lean.Expr) :

Lean.MetaM Lean.Meta.AssertAfterResult

Replace type of the local declaration with id fvarId with one with the same user-facing name, but with type typeNew. This method assumes eqProof is a proof that type of fvarId is equal to typeNew. This tactic actually adds a new declaration and (try to) clear the old one. If the old one cannot be cleared, then at least its user-facing name becomes inaccessible. Remark: the new declaration is added immediately after fvarId. typeNew must be well-formed at fvarId, but eqProof may contain variables declared after fvarId.

Equations