Documentation

Lean.Meta.Tactic.Replace

source
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.
source
def Lean.Meta.replaceTargetEq (mvarId : Lean.MVarId) (targetNew : Lean.Expr) (eqProof : Lean.Expr) :
Lean.MetaM Lean.MVarId
Equations
source
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.
source
def Lean.Meta.replaceTargetDefEq (mvarId : Lean.MVarId) (targetNew : Lean.Expr) :
Lean.MetaM Lean.MVarId
Equations
source
@[inline]
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
source
@[inline]
abbrev Lean.Meta.replaceLocalDecl (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (typeNew : Lean.Expr) (eqProof : Lean.Expr) :
Lean.MetaM Lean.Meta.AssertAfterResult
Equations
source
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.
source
def Lean.Meta.replaceLocalDeclDefEq (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (typeNew : Lean.Expr) :
Lean.MetaM Lean.MVarId
Equations
source
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.
source
def Lean.Meta.change (mvarId : Lean.MVarId) (targetNew : Lean.Expr) (checkDefEq : optParam Bool true) :
Lean.MetaM Lean.MVarId
Equations
source
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.
source
def Lean.Meta.changeLocalDecl (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (typeNew : Lean.Expr) (checkDefEq : optParam Bool true) :
Lean.MetaM Lean.MVarId
Equations
source
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.
source
def Lean.Meta.modifyTarget (mvarId : Lean.MVarId) (f : Lean.Expr → Lean.MetaM Lean.Expr) :
Lean.MetaM Lean.MVarId
Equations
source
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.
source
def Lean.Meta.modifyTargetEqLHS (mvarId : Lean.MVarId) (f : Lean.Expr → Lean.MetaM Lean.Expr) :
Lean.MetaM Lean.MVarId
Equations