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

Revert free variables fvarIds at goal mvarId.

Equations

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

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

Reverts all local declarations after fvarId.

Equations

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

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

Reverts all local declarations starting from fvarId.

Equations

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

def Lean.MVarId.revertAll (mvarId : MVarId) : MetaM MVarId

Reverts all free variables in the goal mvarId. Remark: Auxiliary local declarations are cleared.

Equations

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