def
Lean.MVarId.revert
(mvarId : Lean.MVarId)
(fvarIds : Array Lean.FVarId)
(preserveOrder : optParam Bool false)
(clearAuxDeclsInsteadOfRevert : optParam Bool false)
:
Revert free variables fvarIds at goal mvarId.
Instances For
Reverts all local declarations after fvarId.
Instances For
@[deprecated Lean.MVarId.revert]
def
Lean.Meta.revert
(mvarId : Lean.MVarId)
(fvarIds : Array Lean.FVarId)
(preserveOrder : optParam Bool false)
: