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.withReverted {α : Type} (mvarId : Lean.MVarId) (fvarIds : Array Lean.FVarId) (k : Lean.MVarId → Array Lean.FVarId → Lean.MetaM (α × Array (Option Lean.FVarId) × Lean.MVarId)) (clearAuxDeclsInsteadOfRevert : optParam Bool false) : Lean.MetaM (α × Lean.MVarId)

Runs the continuation k after temporarily reverting some variables from the local context of a metavariable (identified by mvarId), then reintroduces local variables as specified by k.

The argument fvarIds is an array of fvarIds to revert in the order specified. An error is thrown if they cannot be reverted in order.

Once the local variables have been reverted, k is passed mvarId along with an array of local variables that were reverted. This array always has fvarIds as a prefix, but it may contain additional variables that were reverted due to dependencies. k returns a value, a goal, an array of link variables.

Once k has completed, one variable is introduced for each link variable returned by k. If the returned variable is none, the variable is just introduced. If it is some fv, the variable is introduced and then linked as an alias of fv in the info tree. For example, having k return fvars.map .some as the link variables causes all reverted variables to be introduced and linked.

Returns the value returned by k along with the resulting goal.

Equations

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

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

Replaces the type of the free variable fvarId with typeNew.

If checkDefEq is true then an error is thrown if typeNew is not definitionally equal to the type of fvarId. Otherwise this function assumes typeNew and the type of fvarId are definitionally equal.

This function is the same as Lean.MVarId.changeLocalDecl but makes sure to push substitution information into the info tree.

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