Documentation

Batteries.Lean.TagAttribute

source
def Lean.TagAttribute.getDecls (attr : TagAttribute) (env : Environment) :
Array Name

Get the list of declarations tagged with the tag attribute attr.

Equations
    Instances For
      source
      def Lean.TagAttribute.getDecls.core (st : PersistentEnvExtensionState Name NameSet) :
      Array Name

      Implementation of TagAttribute.getDecls.

      Equations
        Instances For