@[inline]

def Lean.Meta.Grind.isSameExpr (a b : Expr) : Bool

Equations

• Lean.Meta.Grind.isSameExpr a b = Lean.Meta.Grind.isSameExpr.unsafe_impl_1 a b

structure Lean.Meta.Grind.ENodeKey : Type

Key for the ENodeMap and ParentMap map. We use pointer addresses and rely on the fact all internalized expressions have been hash-consed, i.e., we have applied shareCommon.

• expr : Expr

instance Lean.Meta.Grind.instHashableENodeKey : Hashable ENodeKey

Equations

• Lean.Meta.Grind.instHashableENodeKey = { hash := fun (k : Lean.Meta.Grind.ENodeKey) => Lean.Meta.Grind.instHashableENodeKey.unsafe_impl_1 k }

instance Lean.Meta.Grind.instBEqENodeKey : BEq ENodeKey

Equations

• Lean.Meta.Grind.instBEqENodeKey = { beq := fun (k₁ k₂ : Lean.Meta.Grind.ENodeKey) => Lean.Meta.Grind.isSameExpr k₁.expr k₂.expr }