Documentation

Lean.Meta.Tactic.Revert

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.

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

    Reverts all local declarations after fvarId.

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

      Reverts all local declarations starting from fvarId.

      Instances For
        source
        def Lean.MVarId.revertAll (mvarId : MVarId) :
        MetaM MVarId

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

        Instances For