Documentation

Lean.Meta.Tactic.Refl

source
def Lean.MVarId.refl (mvarId : Lean.MVarId) :
Lean.MetaM Unit

Close given goal using Eq.refl.

Instances For
    source
    @[deprecated Lean.MVarId.refl]
    def Lean.Meta.refl (mvarId : Lean.MVarId) :
    Lean.MetaM Unit
    Instances For
      source
      @[deprecated Lean.MVarId.refl]
      def Lean.MVarId.applyRefl (mvarId : Lean.MVarId) (msg : optParam Lean.MessageData ((Lean.MessageData.ofFormat ∘ Std.format) "refl failed")) :
      Lean.MetaM Unit
      Instances For
        source
        def Lean.MVarId.heqOfEq (mvarId : Lean.MVarId) :
        Lean.MetaM Lean.MVarId

        Try to apply heq_of_eq. If successful, then return new goal, otherwise return mvarId.

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

          Try to apply eq_of_heq. If successful, then return new goal, otherwise return mvarId.

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

            Close given goal using HEq.refl.

            Instances For