Documentation

Lean.Meta.Sym.Simp.Attr

source
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
Instances For
    source
    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.
    Instances For
      source
      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.
      Instances For
        source
        opaque Lean.Meta.Sym.Simp.symSimpExtension :
        SymSimpExtension
        source
        def Lean.Meta.Sym.Simp.getSymSimpTheorems :
        CoreM Theorems
        Equations
        Instances For