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

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.

@[deprecated Lean.MVarId.replaceTargetEq]

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

Equations

• Lean.Meta.replaceTargetEq mvarId targetNew eqProof = Lean.MVarId.replaceTargetEq mvarId targetNew eqProof

def Lean.MVarId.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.

@[deprecated Lean.MVarId.replaceTargetDefEq]

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

Equations

• Lean.Meta.replaceTargetDefEq mvarId targetNew = Lean.MVarId.replaceTargetDefEq mvarId targetNew

@[inline, reducible]

abbrev Lean.MVarId.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

• Lean.MVarId.replaceLocalDecl mvarId fvarId typeNew eqProof = Lean.Meta.replaceLocalDeclCore mvarId fvarId typeNew eqProof

@[inline, reducible, deprecated Lean.MVarId.replaceLocalDecl]

abbrev Lean.Meta.replaceLocalDecl (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (typeNew : Lean.Expr) (eqProof : Lean.Expr) : Lean.MetaM Lean.Meta.AssertAfterResult

Equations

• Lean.Meta.replaceLocalDecl mvarId fvarId typeNew eqProof = Lean.MVarId.replaceLocalDecl mvarId fvarId typeNew eqProof

def Lean.MVarId.replaceLocalDeclDefEq (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (typeNew : Lean.Expr) : Lean.MetaM Lean.MVarId

Replace the type of fvarId at mvarId with typeNew. Remark: this method assumes that typeNew is definitionally equal to the current type of fvarId.

Equations

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

@[deprecated Lean.MVarId.replaceLocalDeclDefEq]

def Lean.Meta.replaceLocalDeclDefEq (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (typeNew : Lean.Expr) : Lean.MetaM Lean.MVarId

Equations

• Lean.Meta.replaceLocalDeclDefEq mvarId fvarId typeNew = Lean.MVarId.replaceLocalDeclDefEq mvarId fvarId typeNew

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

Replace the target type of mvarId with typeNew. If checkDefEq = false, this method assumes that typeNew is definitionally equal to the current target type. If checkDefEq = true, throw an error if typeNew is not definitionally equal to the current target type.

Equations

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

@[deprecated Lean.MVarId.change]

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

Equations

• Lean.Meta.change mvarId targetNew checkDefEq = Lean.MVarId.withContext mvarId (Lean.MVarId.change mvarId targetNew checkDefEq)

def Lean.MVarId.changeLocalDecl (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (typeNew : Lean.Expr) (checkDefEq : optParam Bool true) : Lean.MetaM Lean.MVarId

Replace the type of the free variable fvarId with typeNew. If checkDefEq = false, this method assumes that typeNew is definitionally equal to fvarId type. If checkDefEq = true, throw an error if typeNew is not definitionally equal to fvarId type.

Equations

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

@[deprecated Lean.MVarId.changeLocalDecl]

def Lean.Meta.changeLocalDecl (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (typeNew : Lean.Expr) (checkDefEq : optParam Bool true) : Lean.MetaM Lean.MVarId

Equations

• Lean.Meta.changeLocalDecl mvarId fvarId typeNew checkDefEq = Lean.MVarId.changeLocalDecl mvarId fvarId typeNew checkDefEq

def Lean.MVarId.modifyTarget (mvarId : Lean.MVarId) (f : Lean.Expr → Lean.MetaM Lean.Expr) : Lean.MetaM Lean.MVarId

Modify mvarId target type using f.

Equations

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

@[deprecated Lean.Meta.modifyTarget]

def Lean.Meta.modifyTarget (mvarId : Lean.MVarId) (f : Lean.Expr → Lean.MetaM Lean.Expr) : Lean.MetaM Lean.MVarId

Equations

• Lean.Meta.modifyTarget mvarId f = Lean.MVarId.modifyTarget mvarId f

def Lean.MVarId.modifyTargetEqLHS (mvarId : Lean.MVarId) (f : Lean.Expr → Lean.MetaM Lean.Expr) : Lean.MetaM Lean.MVarId

Modify mvarId target type left-hand-side using f. Throw an error if target type is not an equality.

Equations

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

@[deprecated Lean.MVarId.modifyTargetEqLHS]

def Lean.Meta.modifyTargetEqLHS (mvarId : Lean.MVarId) (f : Lean.Expr → Lean.MetaM Lean.Expr) : Lean.MetaM Lean.MVarId

Equations

• Lean.Meta.modifyTargetEqLHS mvarId f = Lean.MVarId.modifyTargetEqLHS mvarId f