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

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

Equations

- attr.getDecls env = Lean.TagAttribute.getDecls.core (attr.ext.toEnvExtension.getState env)

Instances For

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

Implementation of `TagAttribute.getDecls`.

Equations

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

Instances For