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 the type of fvarId is equal to typeNew. This tactic actually adds a new declaration and (tries to) clear the old one. If the old one cannot be cleared, then at least its user-facing name becomes inaccessible.

The new local declaration is inserted at the soonest point after fvarId at which it is well-formed. That is, if typeNew involves declarations which occur later than fvarId in the local context, the new local declaration will be inserted immediately after the latest-occurring one. Otherwise, it will be inserted immediately after fvarId.

Note: replaceLocalDecl should not be used when unassigned pending mvars might be present in typeNew, as these may later be synthesized to fvars which occur after fvarId (by e.g. Term.withSynthesize or Term.synthesizeSyntheticMVars) .

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