structure Lean.Meta.Grind.AlphaKey : Type

• expr : Expr

instance Lean.Meta.Grind.instHashableAlphaKey : Hashable AlphaKey

Equations

• Lean.Meta.Grind.instHashableAlphaKey = { hash := fun (k : Lean.Meta.Grind.AlphaKey) => Lean.Meta.Grind.instHashableAlphaKey._private_1 k }

instance Lean.Meta.Grind.instBEqAlphaKey : BEq AlphaKey

Equations

• Lean.Meta.Grind.instBEqAlphaKey = { beq := fun (k₁ k₂ : Lean.Meta.Grind.AlphaKey) => Lean.Meta.Grind.instBEqAlphaKey._private_1 k₁ k₂ }

structure Lean.Meta.Grind.AlphaShareCommon.State : Type

• map : PHashMap ExprPtr Expr
• set : PHashSet AlphaKey

@[reducible, inline]

abbrev Lean.Meta.Grind.AlphaShareCommonM (α : Type) : Type

Equations

• Lean.Meta.Grind.AlphaShareCommonM = StateM Lean.Meta.Grind.AlphaShareCommon.State

def Lean.Meta.Grind.shareCommonAlpha (e : Expr) : AlphaShareCommonM Expr

Similar to shareCommon, but handles alpha-equivalence.

Equations

• Lean.Meta.Grind.shareCommonAlpha e = Lean.Meta.Grind.shareCommonAlpha.go✝ e