- attr : Lean.AttributeImpl
Instances For
def
Lake.OrderedTagAttribute.hasTag
(attr : Lake.OrderedTagAttribute)
(env : Lean.Environment)
(decl : Lake.Name)
:
Instances For
def
Lake.OrderedTagAttribute.getAllEntries
(attr : Lake.OrderedTagAttribute)
(env : Lean.Environment)
:
Get all tagged declaration names, both those imported and those in the current module.