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

Sym Extensions

Extensible state mechanism for SymM, allowing modules to register persistent state that lives across simp invocations within a sym => block. Follows the same pattern as Grind.SolverExtension in Lean/Meta/Tactic/Grind/Types.lean.

opaque Lean.Meta.Sym.SymExtensionStateSpec : (α : Type) × Inhabited α

Opaque extension state type used to store type-erased extension values.

def Lean.Meta.Sym.SymExtensionState : Type

@[implicit_reducible]

instance Lean.Meta.Sym.instInhabitedSymExtensionState : Inhabited SymExtensionState

structure Lean.Meta.Sym.SymExtension (σ : Type) : Type

A registered extension for SymM. Each extension gets a unique index into the extensions array in Sym.State. Can only be created via registerSymExtension.

• id : Nat
• mkInitial : IO σ

@[implicit_reducible]

instance Lean.Meta.Sym.instInhabitedSymExtension {a✝ : Type} : Inhabited (SymExtension a✝)

def Lean.Meta.Sym.instInhabitedSymExtension.default {a✝ : Type} : SymExtension a✝

def Lean.Meta.Sym.registerSymExtension {σ : Type} (mkInitial : IO σ) : IO (SymExtension σ)

Registers a new SymM state extension. Extensions can only be registered during initialization. Returns a handle for typed access to the extension's state.

def Lean.Meta.Sym.SymExtensions.mkInitialStates : IO (Array SymExtensionState)

Returns initial state for all registered extensions.

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

@[implicit_reducible]

instance Lean.Meta.Sym.instInhabitedProofInstArgInfo : Inhabited ProofInstArgInfo

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.

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

@[implicit_reducible]

instance Lean.Meta.Sym.instInhabitedProofInstInfo : Inhabited ProofInstInfo

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.Config : Type

Configuration options for the symbolic computation framework.

• verbose : Bool

  When true, issues are collected during proof search and reported on failure.

@[implicit_reducible]

instance Lean.Meta.Sym.instInhabitedConfig : Inhabited Config

def Lean.Meta.Sym.instInhabitedConfig.default : Config

structure Lean.Meta.Sym.Context : Type

Readonly context for the symbolic computation framework.

• sharedExprs : SharedExprs
• config : Config

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

• cache : Std.HashMap Expr Expr

  Cache for value-level canonicalization (no type reductions applied).

• cacheInType : Std.HashMap Expr Expr

  Cache for type-level canonicalization (reductions applied).

• cacheInsts : Std.HashMap Expr Expr

  Cache mapping instances to their canonical synthesized instances.

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
• defEqI : PHashMap (ExprPtr × ExprPtr) Bool

  Cache for isDefEqI results

• extensions : Array SymExtensionState

  State for registered SymExtensions, indexed by extension id.

• issues : List MessageData

  Issues found during symbolic computation. Accumulated across operations within a sym => block and reported when a tactic fails.

• canon : Canon.State
• debug : Bool

@[reducible, inline]

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

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

def Lean.Meta.Sym.getSharedExprs : SymM SharedExprs

Returns maximally shared commonly used terms

def Lean.Meta.Sym.getTrueExpr : SymM Expr

Returns the internalized True constant.

def Lean.Meta.Sym.isTrueExpr (e : Expr) : SymM Bool

Returns true if e is the internalized True expression.

def Lean.Meta.Sym.getFalseExpr : SymM Expr

Returns the internalized False constant.

def Lean.Meta.Sym.isFalseExpr (e : Expr) : SymM Bool

Returns true if e is the internalized False expression.

def Lean.Meta.Sym.getBoolTrueExpr : SymM Expr

Returns the internalized Bool.true.

def Lean.Meta.Sym.isBoolTrueExpr (e : Expr) : SymM Bool

Returns true if e is the internalized Bool.true expression.

def Lean.Meta.Sym.getBoolFalseExpr : SymM Expr

Returns the internalized Bool.false.

def Lean.Meta.Sym.isBoolFalseExpr (e : Expr) : SymM Bool

Returns true if e is the internalized Bool.false expression.

def Lean.Meta.Sym.getNatZeroExpr : SymM Expr

Returns the internalized 0 : Nat numeral.

def Lean.Meta.Sym.getOrderingEqExpr : SymM Expr

Returns the internalized Ordering.eq.

def Lean.Meta.Sym.getIntExpr : SymM Expr

Returns the internalized Int.

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.

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

@[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

@[inline]

def Lean.Meta.Sym.isDebugEnabled : SymM Bool

Returns true if sym.debug is set

def Lean.Meta.Sym.getConfig : SymM Config

def Lean.Meta.Sym.reportIssue (msg : MessageData) : SymM Unit

Adds an issue message to the issue tracker.

@[inline]

def Lean.Meta.Sym.reportIssueIfVerbose (msg : MessageData) : SymM Unit

Reports an issue if verbose mode is enabled. Does nothing if verbose is false.

def Lean.Meta.Sym.doElemReportIssue!__ : ParserDescr

Reports an issue if verbose mode is enabled.

@[inline]

def Lean.Meta.Sym.reportDbgIssue (msg : MessageData) : SymM Unit

Reports an issue if both verbose and sym.debug are enabled. Does nothing otherwise.

def Lean.Meta.Sym.expandReportDbgIssueMacro (s : Syntax) : MacroM (TSyntax `doElem)

def Lean.Meta.Sym.doElemReportDbgIssue!__ : ParserDescr

Similar to reportIssue!, but only reports issue if sym.debug is set to true.

def Lean.Meta.Sym.getIssues : SymM (List MessageData)

Returns all accumulated issues without clearing them.

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

Runs x with a fresh issue context. Issues reported during x are prepended to the issues that existed before the call.

def Lean.Meta.Sym.isDefEqI (s t : Expr) : SymM Bool

Similar to Meta.isDefEqI, but the result is cache using pointer equality.

@[implicit_reducible]

instance Lean.Meta.Sym.instInhabitedSymM {α : Type} : Inhabited (SymM α)

SymExtension accessors

@[implemented_by _private.Lean.Meta.Sym.SymM.0.Lean.Meta.Sym.SymExtension.getStateCoreImpl]

opaque Lean.Meta.Sym.SymExtension.getStateCore {σ : Type} (ext : SymExtension σ) (extensions : Array SymExtensionState) : IO σ

def Lean.Meta.Sym.SymExtension.getState {σ : Type} (ext : SymExtension σ) : SymM σ

@[implemented_by _private.Lean.Meta.Sym.SymM.0.Lean.Meta.Sym.SymExtension.modifyStateImpl]

opaque Lean.Meta.Sym.SymExtension.modifyState {σ : Type} (ext : SymExtension σ) (f : σ → σ) : SymM Unit