Documentation

Lean.Meta.Tactic.Grind.EMatchTheoremPtr

source
@[inline]
def Lean.Meta.Grind.isSameEMatchTheoremPtr (a b : EMatchTheorem) :
Bool
Equations
    Instances For
      source
      structure Lean.Meta.Grind.EMatchTheoremPtr :
      Type
      Instances For
        source
        @[reducible, inline]
        abbrev Lean.Meta.Grind.hashEMatchTheoremPtr (thm : EMatchTheorem) :
        UInt64
        Equations
          Instances For
            source
            instance Lean.Meta.Grind.instHashableEMatchTheoremPtr :
            Hashable EMatchTheoremPtr
            Equations
              source
              instance Lean.Meta.Grind.instBEqEMatchTheoremPtr :
              BEq EMatchTheoremPtr
              Equations