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

Instances For

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

Instances For

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

Instances For