Documentation

Lean.Meta.Tactic.Grind.EMatchTheoremPtr

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