Documentation

Std.Lean.TagAttribute

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

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

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

    Implementation of TagAttribute.getDecls.

    Instances For