def Lean.MVarId.revert (mvarId : Lean.MVarId) (fvarIds : Array Lean.FVarId) (preserveOrder clearAuxDeclsInsteadOfRevert : Bool := false) : Lean.MetaM (Array Lean.FVarId × Lean.MVarId)

Revert free variables fvarIds at goal mvarId.

def Lean.MVarId.revertAfter (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) : Lean.MetaM (Array Lean.FVarId × Lean.MVarId)

Reverts all local declarations after fvarId.

Equations

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