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.

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

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

Equations

• thms.insert thm = { thms := Lean.Meta.Sym.insertPattern thms.thms thm.pattern thm }

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

Equations

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

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

Equations

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

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

Equations

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