def Lean.Meta.Sym.Simp.addSymSimpTheorem (ext : SymSimpExtension) (declName : Name) (attrKind : AttributeKind) : MetaM Unit

Adds a Sym.Simp theorem (an equality) to the given extension.

Equations

• Lean.Meta.Sym.Simp.addSymSimpTheorem ext declName attrKind = do let thm ← Lean.Meta.Sym.Simp.mkTheoremFromDecl declName Lean.ScopedEnvExtension.add ext thm attrKind

def Lean.Meta.Sym.Simp.addSymSimpDecl (ext : SymSimpExtension) (declName : Name) (attrKind : AttributeKind) (validate : Name → MetaM Unit := fun (x : Name) => pure ()) : MetaM Unit

Adds a declaration to the given Sym.Simp theorem extension. When declName is a proposition, it is added as a rewrite theorem. When it is a definition, its equational theorems are added, and its unfolding theorem as a fallback. See getSimpTheoremNames.

Equations

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

def Lean.Meta.Sym.Simp.mkSymSimpAttr (attrName : Name) (attrDescr : String) (ext : SymSimpExtension) (ref : Name := by exact decl_name%) : IO Unit

Creates a Sym.Simp attribute for a named theorem set. When a proposition is tagged, it is added as a rewrite theorem. When a definition is tagged, its equation theorems are added.

Equations

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

def Lean.Meta.Sym.Simp.registerSymSimpAttr (attrName : Name) (attrDescr : String) (ref : Name := by exact decl_name%) : IO SymSimpExtension

Registers a named Sym.Simp theorem set. Each set gets its own attribute and its own SymSimpExtension (persistent environment extension).

Must be called during initialization.

Equations

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

opaque Lean.Meta.Sym.Simp.symSimpExtension : SymSimpExtension

def Lean.Meta.Sym.Simp.getSymSimpTheorems : CoreM Theorems

Equations

• Lean.Meta.Sym.Simp.getSymSimpTheorems = Lean.Meta.Sym.Simp.symSimpExtension.getTheorems