@[inline]

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

structure Lean.Meta.Sym.ExprPtr : Type

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

• expr : Expr

@[reducible, inline]

abbrev Lean.Meta.Sym.hashPtrExpr (e : Expr) : UInt64

@[implicit_reducible]

instance Lean.Meta.Sym.instHashableExprPtr : Hashable ExprPtr

@[implicit_reducible]

instance Lean.Meta.Sym.instBEqExprPtr : BEq ExprPtr