def Lean.MVarId.replaceTargetEq (mvarId : MVarId) (targetNew eqProof : Expr) : MetaM 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.

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

Converts 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.

If targetNew is equal to target, then returns mvarId unchanged. Uses Expr.equal for the comparison so that it is possible to update binder names, etc., which are user-visible.

Equations

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

@[inline]

def Lean.MVarId.replaceLocalDecl (mvarId : MVarId) (fvarId : FVarId) (typeNew eqProof : Expr) : MetaM 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

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

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

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

If typeNew is equal to current type of fvarId, then returns mvarId unchanged. Uses Expr.equal for the comparison so that it is possible to update binder names, etc., which are user-visible.

Equations

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

def Lean.MVarId.change (mvarId : MVarId) (targetNew : Expr) (checkDefEq : Bool := true) : MetaM 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.

def Lean.MVarId.withReverted {α : Type} (mvarId : MVarId) (fvarIds : Array FVarId) (k : MVarId → Array FVarId → MetaM (α × Array (Option FVarId) × MVarId)) (clearAuxDeclsInsteadOfRevert : Bool := false) : MetaM (α × MVarId)

Executes the revert/intro pattern, running the continuation k after temporarily reverting the given local variables from the local context of the metavariable mvarId, and then re-introducing the local variables specified by k.

• mvarId is the goal metavariable to operate on.
• fvarIds is an array of fvarIds to revert in the order specified. An error is thrown if they cannot be reverted in order.
• clearAuxDeclsInsteadOfRevert is configuration passed to Lean.MVarId.revert.
• k is the continuation run once the local variables have been reverted. It is provided mvarId after the requested variables have been reverted along with the array of reverted variables. This array always contains fvarIds, but it may contain additional variables that were reverted due to dependencies. The continuation returns a value, a new goal, and an aliasing array.

Once k has completed, one variable is introduced per entry in the aliasing array.

• If the entry is none, the variable is just introduced.
• If the entry is some fv (where fv is a variable from fvarIds), the variable is introduced and then recorded as an alias of fv in the info tree. This for example causes the unused variable linter as seeing fv and this newly introduced variable as being "the same".

For example, if k leaves all the reverted variables in the same order, having it return fvars.map .some as the aliasing array causes those variables to be re-introduced and aliased to the original local variables.

Returns the value returned by k along with the resulting goal after variable introduction.

See Lean.MVarId.changeLocalDecl for an example. The motivation is that to work on a local variable, you need to move it into the goal, alter the goal, and then bring it back into the local context, all while keeping track of any other local variables that depend on this one.

Equations

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

def Lean.MVarId.withRevertedFrom {α : Type} (mvarId : MVarId) (fvarId : FVarId) (k : MVarId → Array FVarId → MetaM (α × Array (Option FVarId) × MVarId)) : MetaM (α × MVarId)

Like Lean.MVarId.withReverted, but reverts all local variables starting from fvarId.

Equations

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

def Lean.MVarId.changeLocalDecl (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr) (checkDefEq : Bool := true) : MetaM 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.

Equations

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

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

Modify mvarId target type using f.

Equations

• mvarId.modifyTarget f = mvarId.withContext do mvarId.checkNotAssigned `modifyTarget let __do_lift ← mvarId.getType let __do_lift ← f __do_lift mvarId.change __do_lift false

def Lean.MVarId.modifyTargetEqLHS (mvarId : MVarId) (f : Expr → MetaM Expr) : MetaM 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.

def Lean.MVarId.clearValue (mvarId : MVarId) (fvarId : FVarId) : MetaM MVarId

Clears the value of the local definition fvarId. Ensures that the resulting goal state is still type correct. Throws an error if it is a local hypothesis without a value.

Preserves the order of the local context.

Equations

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