opaque Lean.Meta.Sym.sym.debug : Lean.Option Bool

structure Lean.Meta.Sym.ProofInstArgInfo : Type

Information about a single argument position in a function's type signature.

This is used during pattern matching and structural definitional equality tests to identify arguments that can be skipped or handled specially (e.g., instance arguments can be synthesized, proof arguments can be inferred).

• isProof : Bool

  true if this argument is a proof (its type is a Prop).

• isInstance : Bool

  true if this argument is a type class instance.

def Lean.Meta.Sym.instInhabitedProofInstArgInfo.default : ProofInstArgInfo

Equations

• Lean.Meta.Sym.instInhabitedProofInstArgInfo.default = { isProof := default, isInstance := default }

instance Lean.Meta.Sym.instInhabitedProofInstArgInfo : Inhabited ProofInstArgInfo

Equations

• Lean.Meta.Sym.instInhabitedProofInstArgInfo = { default := Lean.Meta.Sym.instInhabitedProofInstArgInfo.default }

structure Lean.Meta.Sym.ProofInstInfo : Type

Information about a function symbol. It stores which argument positions are proofs or instances, enabling optimizations during pattern matching and structural definitional equality tests such as skipping proof arguments or deferring instance synthesis.

• argsInfo : Array ProofInstArgInfo

  Information about each argument position.

instance Lean.Meta.Sym.instInhabitedProofInstInfo : Inhabited ProofInstInfo

Equations

• Lean.Meta.Sym.instInhabitedProofInstInfo = { default := Lean.Meta.Sym.instInhabitedProofInstInfo.default }

def Lean.Meta.Sym.instInhabitedProofInstInfo.default : ProofInstInfo

Equations

• Lean.Meta.Sym.instInhabitedProofInstInfo.default = { argsInfo := default }

inductive Lean.Meta.Sym.CongrInfo : Type

Information on how to build congruence proofs for function applications. This enables efficient rewriting of subterms without repeatedly inferring types or instances.

• none : CongrInfo

  None of the arguments of the function can be rewritten.

• fixedPrefix (prefixSize suffixSize : Nat) : CongrInfo

  For functions with a fixed prefix of implicit/instance arguments followed by explicit non-dependent arguments that can be rewritten independently.

  • prefixSize: Number of leading arguments (types, instances) that are determined by the suffix arguments and should not be rewritten directly.
  • suffixSize: Number of trailing arguments that can be rewritten using simple congruence.

  Examples (showing prefixSize, suffixSize):

  • HAdd.hAdd {α β γ} [HAdd α β γ] (a : α) (b : β): (4, 2) — rewrite a and b
  • And (p q : Prop): (0, 2) — rewrite both propositions
  • Eq {α} (a b : α): (1, 2) — rewrite a and b, type α is fixed
  • Neg.neg {α} [Neg α] (a : α): (2, 1) — rewrite just a
• interlaced (rewritable : Array Bool) : CongrInfo

  For functions with interlaced rewritable and non-rewritable arguments. Each element indicates whether the corresponding argument position can be rewritten.

  Example: For HEq {α : Sort u} (a : α) {β : Sort u} (b : β), the mask would be #[false, true, false, true] — we can rewrite a and b, but not α or β.

• congrTheorem (thm : CongrTheorem) : CongrInfo

  For functions that have proofs and Decidable arguments. For this kind of function we generate a custom theorem. Example: Array.eraseIdx {α : Type u} (xs : Array α) (i : Nat) (h : i < xs.size) : Array α. The proof argument h depends on xs and i. To be able to rewrite xs and i, we use the auto-generated theorem.

  Array.eraseIdx.congr_simp {α : Type u} (xs xs' : Array α) (e_xs : xs = xs')
      (i i' : Nat) (e_i : i = i') (h : i < xs.size) : xs.eraseIdx i h = xs'.eraseIdx i' ⋯
  

structure Lean.Meta.Sym.SharedExprs : Type

Pre-shared expressions for commonly used terms.

• trueExpr : Expr
• falseExpr : Expr
• natZExpr : Expr
• btrueExpr : Expr
• bfalseExpr : Expr
• ordEqExpr : Expr
• intExpr : Expr

structure Lean.Meta.Sym.Context : Type

Readonly context for the symbolic computation framework.

• sharedExprs : SharedExprs

structure Lean.Meta.Sym.State : Type

Mutable state for the symbolic computation framework.

• share : AlphaShareCommon.State

  ShareCommon (aka Hash-consing) state.

• maxFVar : PHashMap ExprPtr (Option FVarId)

  Maps expressions to their maximal free variable (by declaration index).

  • maxFVar[e] = some fvarId means fvarId is the free variable with the largest declaration index occurring in e.
  • maxFVar[e] = none means e contains no free variables (but may contain metavariables).

  Recall that if e contains a metavariable ?m, then we assume e may contain any free variable in the local context associated with ?m.

  This mapping enables O(1) local context compatibility checks during metavariable assignment. Instead of traversing local contexts with isSubPrefixOf, we check if the maximal free variable in the assigned value is in scope of the metavariable's local context.

  Note: We considered using a mapping PHashMap ExprPtr FVarId. However, there is a corner case that is not supported by this representation. e contains a metavariable (with an empty local context), and no free variables.

• proofInstInfo : PHashMap Name (Option ProofInstInfo)
• inferType : PHashMap ExprPtr Expr

  Cache for inferType results, keyed by pointer equality. SymM uses a fixed configuration, so we can use a simpler key than MetaM. Remark: type inference is a bottleneck on Meta.Tactic.Simp simplifier.

• getLevel : PHashMap ExprPtr Level

  Cache for getLevel results, keyed by pointer equality.

• congrInfo : PHashMap ExprPtr CongrInfo
• debug : Bool

@[reducible, inline]

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

Equations

• Lean.Meta.Sym.SymM = ReaderT Lean.Meta.Sym.Context (StateRefT' IO.RealWorld Lean.Meta.Sym.State Lean.MetaM)

def Lean.Meta.Sym.SymM.run {α : Type} (x : SymM α) : MetaM α

Equations

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

def Lean.Meta.Sym.getSharedExprs : SymM SharedExprs

Returns maximally shared commonly used terms

Equations

• Lean.Meta.Sym.getSharedExprs = do let __do_lift ← read pure __do_lift.sharedExprs

def Lean.Meta.Sym.getTrueExpr : SymM Expr

Returns the internalized True constant.

Equations

• Lean.Meta.Sym.getTrueExpr = do let __do_lift ← Lean.Meta.Sym.getSharedExprs pure __do_lift.trueExpr

def Lean.Meta.Sym.getFalseExpr : SymM Expr

Returns the internalized False constant.

Equations

• Lean.Meta.Sym.getFalseExpr = do let __do_lift ← Lean.Meta.Sym.getSharedExprs pure __do_lift.falseExpr

def Lean.Meta.Sym.getBoolTrueExpr : SymM Expr

Returns the internalized Bool.true.

Equations

• Lean.Meta.Sym.getBoolTrueExpr = do let __do_lift ← Lean.Meta.Sym.getSharedExprs pure __do_lift.btrueExpr

def Lean.Meta.Sym.getBoolFalseExpr : SymM Expr

Returns the internalized Bool.false.

Equations

• Lean.Meta.Sym.getBoolFalseExpr = do let __do_lift ← Lean.Meta.Sym.getSharedExprs pure __do_lift.bfalseExpr

def Lean.Meta.Sym.getNatZeroExpr : SymM Expr

Returns the internalized 0 : Nat numeral.

Equations

• Lean.Meta.Sym.getNatZeroExpr = do let __do_lift ← Lean.Meta.Sym.getSharedExprs pure __do_lift.natZExpr

def Lean.Meta.Sym.getOrderingEqExpr : SymM Expr

Returns the internalized Ordering.eq.

Equations

• Lean.Meta.Sym.getOrderingEqExpr = do let __do_lift ← Lean.Meta.Sym.getSharedExprs pure __do_lift.ordEqExpr

def Lean.Meta.Sym.getIntExpr : SymM Expr

Returns the internalized Int.

Equations

• Lean.Meta.Sym.getIntExpr = do let __do_lift ← Lean.Meta.Sym.getSharedExprs pure __do_lift.intExpr

def Lean.Meta.Sym.shareCommon (e : Expr) : SymM Expr

Applies hash-consing to e. Recall that all expressions in a grind goal have been hash-consed. We perform this step before we internalize expressions.

Equations

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

def Lean.Meta.Sym.shareCommonInc (e : Expr) : SymM Expr

Incremental variant of shareCommon 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.

Unlike shareCommon, 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 ← shareCommonInc result -- efficiently restore sharing

Equations

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

@[reducible, inline]

abbrev Lean.Meta.Sym.share (e : Expr) : SymM Expr

Incremental variant of shareCommon 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.

Unlike shareCommon, 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 ← shareCommonInc result -- efficiently restore sharing

Equations

• Lean.Meta.Sym.share e = Lean.Meta.Sym.shareCommonInc e

@[inline]

def Lean.Meta.Sym.isDebugEnabled : SymM Bool

Returns true if sym.debug is set

Equations

• Lean.Meta.Sym.isDebugEnabled = do let __do_lift ← get pure __do_lift.debug