Documentation

Lean.Meta.Tactic.Clear

source
def Lean.MVarId.clear (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) :
Lean.MetaM Lean.MVarId

Erase the given free variable from the goal mvarId.

Instances For
    source
    @[deprecated Lean.MVarId.clear]
    def Lean.Meta.clear (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) :
    Lean.MetaM Lean.MVarId
    Instances For
      source
      def Lean.MVarId.tryClear (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) :
      Lean.MetaM Lean.MVarId

      Try to erase the given free variable from the goal mvarId. It is no-op if the free variable cannot be erased due to forward dependencies.

      Instances For
        source
        @[deprecated Lean.MVarId.tryClear]
        def Lean.Meta.tryClear (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) :
        Lean.MetaM Lean.MVarId
        Instances For
          source
          def Lean.MVarId.tryClearMany (mvarId : Lean.MVarId) (fvarIds : Array Lean.FVarId) :
          Lean.MetaM Lean.MVarId

          Try to erase the given free variables from the goal mvarId.

          Instances For
            source
            @[deprecated Lean.MVarId.tryClearMany]
            def Lean.Meta.tryClearMany (mvarId : Lean.MVarId) (fvarIds : Array Lean.FVarId) :
            Lean.MetaM Lean.MVarId
            Instances For