source
structure Lean.Meta.Grind.AlphaKey :
Type

- expr : Expr

Instances For

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

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

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

- map : PHashMap ExprPtr Expr
- set : PHashSet AlphaKey

Instances For

source
@[reducible, inline]
abbrev Lean.Meta.Grind.AlphaShareCommonM (α : Type) :
Type
Equations

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

Instances For

source
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

Instances For