Implementation of the change at h tactic

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)

Function to help do the revert/intro pattern, running some code inside a context where certain variables have been reverted before re-introing them. It will push FVarId alias information into info trees for you according to a simple protocol.

• fvarIds is an array of fvarIds to revert. These are passed to Lean.MVarId.revert with preserveOrder := true, hence the function raises an error if they cannot be reverted in the provided order.
• k is given the goal with all the variables reverted and the array of reverted FVarIds, with the requested FVarIds at the beginning. It must return a tuple of a value, an array describing which FVarIds to link, and a mutated MVarId.

The a : Array (Option FVarId) array returned by k is interpreted in the following way. The function will intro a.size variables, and then for each non-none entry we create an FVar alias between it and the corresponding introed variable. For example, having k return fvars.map .some causes all reverted variables to be introed 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

Replace the type of the free variable fvarId with typeNew.

If checkDefEq = true then throws an error 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 infotree.

Equations

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