Documentation

Lean.Meta.Tactic.Simp.Attr

def Lean.Meta.mkSimpAttr (attrName : Name) (attrDescr : String) (ext : SimpExtension) (ref : Name := by exact decl_name%) :
Equations
    Instances For
      def Lean.Meta.registerSimpAttr (attrName : Name) (attrDescr : String) (ref : Name := by exact decl_name%) :

      Registers the given name as a custom simp set. Applying the name as an attribute to a name adds it to the simp set, and using the name as a parameter to the simp tactic causes simp to use the included lemmas.

      Custom simp sets must be registered during initialization.

      The description should be a short, singular noun phrase that describes the contents of the custom simp set.

      Equations
        Instances For