structure Lean.Meta.Sym.Simp.Theorem : Type

A simplification theorem for the structural simplifier.

Contains both the theorem expression and a precomputed pattern for efficient unification during rewriting.

• expr : Expr

  The theorem expression, typically Expr.const declName for a named theorem.

• pattern : Pattern

  Precomputed pattern extracted from the theorem's type for efficient matching.

• rhs : Expr

  Right-hand side of the equation.

• perm : Bool

  If true, the theorem is a permutation rule (e.g., x + y = y + x). Rewriting is only applied when the result is strictly less than the input (using acLt), preventing infinite loops.

• rhsVarMask : Nat

  Bitmask of the pattern variables that occur in rhs: bit i is set iff pattern variable i occurs in rhs. Theorem.rewrite uses it to detect hypothesis proofs that become part of the resulting term and must consequently be maximally shared.

• fallback : Bool

  If true, the theorem is tried only when no other theorem rewrites the term. Used for the unfolding theorem f.eq_def of a definition f provided as a Sym.simp parameter: the equational theorems of f take precedence. See Theorems.rewrite.

@[instance_reducible]

instance Lean.Meta.Sym.Simp.instInhabitedTheorem : Inhabited Theorem

Equations

• Lean.Meta.Sym.Simp.instInhabitedTheorem = { default := Lean.Meta.Sym.Simp.instInhabitedTheorem.default }

@[instance_reducible]

instance Lean.Meta.Sym.Simp.instBEqTheorem : BEq Theorem

Equations

• Lean.Meta.Sym.Simp.instBEqTheorem = { beq := fun (thm₁ thm₂ : Lean.Meta.Sym.Simp.Theorem) => thm₁.expr == thm₂.expr }

structure Lean.Meta.Sym.Simp.Theorems : Type

Collection of simplification theorems available to the simplifier.

• thms : DiscrTree Theorem
• fallback : DiscrTree Theorem

  The theorems with Theorem.fallback := true. See Theorems.rewrite.

@[instance_reducible]

instance Lean.Meta.Sym.Simp.instInhabitedTheorems : Inhabited Theorems

Equations

• Lean.Meta.Sym.Simp.instInhabitedTheorems = { default := Lean.Meta.Sym.Simp.instInhabitedTheorems.default }

def Lean.Meta.Sym.Simp.Theorems.isEmpty (thms : Theorems) : Bool

Equations

• thms.isEmpty = (thms.thms.root.isEmpty && thms.fallback.root.isEmpty)

def Lean.Meta.Sym.Simp.Theorems.insert (thms : Theorems) (thm : Theorem) : Theorems

Equations

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

def Lean.Meta.Sym.Simp.Theorems.getMatch (thms : Theorems) (mctx : MetavarContext) (e : Expr) : Array Theorem

Returns the theorems matching e, excluding the fallback ones.

Equations

• thms.getMatch mctx e = Lean.Meta.Sym.getMatch mctx thms.thms e

def Lean.Meta.Sym.Simp.Theorems.getMatchWithExtra (thms : Theorems) (mctx : MetavarContext) (e : Expr) : Array (Theorem × Nat)

Returns the theorems matching a prefix of e, excluding the fallback ones.

Equations

• thms.getMatchWithExtra mctx e = Lean.Meta.Sym.getMatchWithExtra mctx thms.thms e

def Lean.Meta.Sym.Simp.Theorems.getFallbackMatchWithExtra (thms : Theorems) (mctx : MetavarContext) (e : Expr) : Array (Theorem × Nat)

Returns the fallback theorems matching a prefix of e.

Equations

• thms.getFallbackMatchWithExtra mctx e = Lean.Meta.Sym.getMatchWithExtra mctx thms.fallback e

def Lean.Meta.Sym.Simp.isPerm (numVars : Nat) (lhs rhs : Expr) : Bool

Equations

• Lean.Meta.Sym.Simp.isPerm numVars lhs rhs = match (ReaderT.run (Lean.Meta.Sym.Simp.isPermAux✝ lhs rhs) 0).run (Array.replicate numVars none) with | Except.ok a => true | x => false

def Lean.Meta.Sym.Simp.mkTheoremFromDecl (declName : Name) : MetaM Theorem

Create a Theorem from a declaration. Handles equalities, ¬, ↔, and propositions.

Equations

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

def Lean.Meta.Sym.Simp.mkTheoremFromExpr (e : Expr) : MetaM Theorem

Create a Theorem from a proof expression. Handles equalities, ¬, ↔, and propositions.

Equations

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

structure Lean.Meta.Sym.Simp.DeclTheoremNames : Type

The names of the theorems contributed by a declaration used as a Sym.simp theorem.

• thms : Array Name

  The declaration itself when it is a proposition, or the equational theorems of a definition. Empty for a reducible definition, which the Sym preprocessing unfolds.

• unfold? : Option Name

  The unfolding theorem f.eq_def of a non-recursive definition f, unless thms already unfolds every f application. It is a fallback (see Theorem.fallback), so that simp [f] unfolds the f applications not covered by the equational theorems, like Meta.simp does.

def Lean.Meta.Sym.Simp.getSimpTheoremNames (declName : Name) : MetaM DeclTheoremNames

Returns the names of the theorems contributed by declName when it is used as a Sym.simp theorem. A proposition contributes itself. A definition contributes its equational theorems and, when it is not recursive, its unfolding theorem, so that simp [f] unfolds f applications.

Equations

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

def Lean.Meta.Sym.Simp.mkTheoremsFromDecl (declName : Name) : MetaM (Array Theorem)

Creates the Theorems contributed by declName when it is used as a Sym.simp theorem. See getSimpTheoremNames.

Equations

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

@[reducible, inline]

abbrev Lean.Meta.Sym.Simp.SymSimpExtension : Type

Environment extension storing a set of Sym.Simp theorems. Each named set gets its own extension, created by registerSymSimpAttr.

Equations

• Lean.Meta.Sym.Simp.SymSimpExtension = Lean.SimpleScopedEnvExtension Lean.Meta.Sym.Simp.Theorem Lean.Meta.Sym.Simp.Theorems

def Lean.Meta.Sym.Simp.SymSimpExtension.getTheorems (ext : SymSimpExtension) : CoreM Theorems

Equations

• ext.getTheorems = do let __do_lift ← Lean.getEnv pure (Lean.ScopedEnvExtension.getState ext __do_lift)

def Lean.Meta.Sym.Simp.mkSymSimpExt (name : Name := by exact decl_name%) : IO SymSimpExtension

Equations

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

@[reducible, inline]

abbrev Lean.Meta.Sym.Simp.SymSimpExtensionMap : Type

Equations

• Lean.Meta.Sym.Simp.SymSimpExtensionMap = Std.HashMap Lean.Name Lean.Meta.Sym.Simp.SymSimpExtension

opaque Lean.Meta.Sym.Simp.symSimpExtensionMapRef : IO.Ref SymSimpExtensionMap

def Lean.Meta.Sym.Simp.getSymSimpExtension? (attrName : Name) : CoreM (Option SymSimpExtension)

Equations

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