Documentation

Lean.Meta.Tactic.Revert

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

Revert free variables fvarIds at goal mvarId.

Equations
    Instances For

      Reverts all local declarations after fvarId.

      Equations
        Instances For