def Lean.Meta.Sym.isGrindGadget (declName : Name) : Bool

Returns true if declName is the name of a grind helper declaration that should not be unfolded by unfoldReducible. Grind.EqMatch, Grind.MatchCond, Grind.nestedReducible are abbrevs, but they are gadgets that must survive until the corresponding propagators consume them.

Equations

• Lean.Meta.Sym.isGrindGadget declName = (declName == `Lean.Grind.EqMatch || declName == `Lean.Grind.MatchCond || declName == `Lean.Grind.nestedDecidable)

def Lean.Meta.Sym.isUnfoldReducibleCandidate (env : Environment) (declName : Name) : Bool

Returns true if declName is a reducible constant that the unfoldReducible preprocessing step must unfold.

Projection functions are excluded even though they are reducible by default: unfolding them produces kernel projections, which the foldProjs preprocessing step folds back into projection function applications.

Equations

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

structure Lean.Meta.Sym.AlphaKey : Type

• expr : Expr

@[instance_reducible]

instance Lean.Meta.Sym.instHashableAlphaKey : Hashable AlphaKey

Equations

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

@[instance_reducible]

instance Lean.Meta.Sym.instBEqAlphaKey : BEq AlphaKey

Equations

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

structure Lean.Meta.Sym.AlphaShareCommon.Context : Type

Readonly context for AlphaShareCommonM.

• env : Environment
• checkReducible : Bool

  When true, shareCommonAlpha and shareCommonAlphaInc throw when hash-consing a new reducible constant that the unfoldReducible preprocessing step should have unfolded (see isUnfoldReducibleCandidate).

• checkProj : Bool

  When true, shareCommonAlpha and shareCommonAlphaInc throw when hash-consing a new kernel projection (Expr.proj), which the foldProjs preprocessing step should have folded.

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

• set : PHashSet AlphaKey

@[reducible, inline]

abbrev Lean.Meta.Sym.AlphaShareCommon.Cache : Type

Cache used by shareCommonAlpha to avoid visiting the same subterm (by pointer) of a DAG-shaped input over and over again. It maps visited subterms to their maximally shared results. Note that the ExprPtr keys own their expressions, so the cached subterms are kept alive while the cache is alive and their pointers cannot be recycled.

Equations

• Lean.Meta.Sym.AlphaShareCommon.Cache = Std.HashMap Lean.Meta.Sym.ExprPtr Lean.Expr

@[reducible, inline]

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

Monad for hash-consing expressions up to alpha-equivalence.

When checks are enabled in the context, hash-consing throws if a new term violates the SymM representation invariants (reducible constants unfolded, kernel projections folded). Terms already in the state are never re-checked: membership certifies that a term was admitted before. On a throw, the state contains every term hash-consed before the failure; these terms individually satisfy the invariants, so callers should keep the partial state and retry after repairing the input term. The error value is the Cache accumulated before the failure (empty for shareCommonAlphaInc, which does not use one); the retry can be seeded with it to avoid revisiting the subterms processed before the failure.

Equations

• Lean.Meta.Sym.AlphaShareCommonM = ReaderT Lean.Meta.Sym.AlphaShareCommon.Context (EStateM Lean.Meta.Sym.AlphaShareCommon.Cache Lean.Meta.Sym.AlphaShareCommon.State)

@[inline]

def Lean.Meta.Sym.shareCommonAlpha (e : Expr) (cache : AlphaShareCommon.Cache := ∅) : AlphaShareCommonM Expr

Similar to shareCommon, but handles alpha-equivalence.

cache may contain the results of a previous run that failed with a check violation (see AlphaShareCommonM); seeding the retry with it avoids revisiting the subterms that were processed before the failure.

Equations

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

@[inline]

def Lean.Meta.Sym.shareCommonAlphaInc (e : Expr) : AlphaShareCommonM Expr

Incremental variant of shareCommonAlpha for expressions constructed from already-shared subterms.

Use this when an expression e was produced by a Lean API (e.g., inferType, mkApp4) that does not preserve maximal sharing, but the inputs to that API were already maximally shared. In this case, only the newly constructed nodes need processing—the shared subterms can be looked up directly in the AlphaShareCommonM state without building a temporary hashmap.

Unlike shareCommonAlpha, this function does not use a local Std.HashMap ExprPtr Expr to track visited nodes. This is more efficient when the number of new (unshared) nodes is small, which is the common case when wrapping API calls that build a few constructor nodes around shared inputs.

Example:

-- `a` and `b` are already maximally shared
let result := mkApp2 f a b  -- result is not maximally shared
let result ← shareCommonAlphaInc result -- efficiently restore sharing

Equations

• Lean.Meta.Sym.shareCommonAlphaInc e = Lean.Meta.Sym.shareCommonAlphaInc.go✝ e