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.alphaHash✝ k.expr }

instance Lean.Meta.Grind.instBEqAlphaKey : BEq AlphaKey

Equations

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

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

• map : PHashMap ENodeKey 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

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

Equations

• One or more equations did not get rendered due to their size.