Documentation

Lean.Meta.Sym.AlphaShareCommon

source
structure Lean.Meta.Sym.AlphaKey :
Type
Instances For
    source
    instance Lean.Meta.Sym.instHashableAlphaKey :
    Hashable AlphaKey
    Equations
    source
    instance Lean.Meta.Sym.instBEqAlphaKey :
    BEq AlphaKey
    Equations
    source
    structure Lean.Meta.Sym.AlphaShareCommon.State :
    Type
    Instances For
      source
      @[reducible, inline]
      abbrev Lean.Meta.Sym.AlphaShareCommonM (α : Type) :
      Type
      Equations
      Instances For
        source
        @[inline]
        def Lean.Meta.Sym.shareCommonAlpha (e : Expr) :
        AlphaShareCommonM Expr

        Similar to shareCommon, but handles alpha-equivalence.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[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
          Instances For