ink

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

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

Equations

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

ink

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

Implementation of TagAttribute.getDecls.

Equations

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