← Copula mathematical handbook

@[inline]

def Lean.Meta.Grind.isSameEMatchTheoremPtr (a b : EMatchTheorem) : Bool

Equations

• Lean.Meta.Grind.isSameEMatchTheoremPtr a b = Lean.Meta.Grind.isSameEMatchTheoremPtr.unsafe_impl_2✝ a b

structure Lean.Meta.Grind.EMatchTheoremPtr : Type

• thm : EMatchTheorem

@[reducible, inline]

abbrev Lean.Meta.Grind.hashEMatchTheoremPtr (thm : EMatchTheorem) : UInt64

Equations

• Lean.Meta.Grind.hashEMatchTheoremPtr thm = Lean.Meta.Grind.hashEMatchTheoremPtr.unsafe_impl_2 thm

@[instance_reducible]

instance Lean.Meta.Grind.instHashableEMatchTheoremPtr : Hashable EMatchTheoremPtr

Equations

• Lean.Meta.Grind.instHashableEMatchTheoremPtr = { hash := fun (k : Lean.Meta.Grind.EMatchTheoremPtr) => Lean.Meta.Grind.hashEMatchTheoremPtr k.thm }

@[instance_reducible]

instance Lean.Meta.Grind.instBEqEMatchTheoremPtr : BEq EMatchTheoremPtr

Equations

• Lean.Meta.Grind.instBEqEMatchTheoremPtr = { beq := fun (k₁ k₂ : Lean.Meta.Grind.EMatchTheoremPtr) => Lean.Meta.Grind.isSameEMatchTheoremPtr k₁.thm k₂.thm }