Documentation

Lean.Meta.Tactic.Grind.EMatchTheoremPtr

@[inline]

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

Equations

Lean.Meta.Grind.isSameEMatchTheoremPtr a b = Lean.Meta.Grind.isSameEMatchTheoremPtr.unsafe_impl_3✝ a b

Instances For

structure Lean.Meta.Grind.EMatchTheoremPtr :

thm : EMatchTheorem

Instances For

@[reducible, inline]

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

Equations

Lean.Meta.Grind.hashEMatchTheoremPtr thm = Lean.Meta.Grind.hashEMatchTheoremPtr.unsafe_impl_3 thm

Instances For

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 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 }