structure Lake.OrderedTagAttribute : Type

• attr : Lean.AttributeImpl
• ext : Lean.PersistentEnvExtension Lean.Name Lean.Name (Array Lean.Name)

instance Lake.instInhabitedOrderedTagAttribute : Inhabited OrderedTagAttribute

def Lake.registerOrderedTagAttribute (name : Lean.Name) (descr : String) (validate : Lean.Name → Lean.AttrM Unit := fun (x : Lean.Name) => pure ()) (ref : Lean.Name := by exact decl_name%) : IO OrderedTagAttribute

def Lake.OrderedTagAttribute.hasTag (attr : OrderedTagAttribute) (env : Lean.Environment) (decl : Lean.Name) : Bool

def Lake.OrderedTagAttribute.getAllEntries (attr : OrderedTagAttribute) (env : Lean.Environment) : Array Lean.Name

Get all tagged declaration names, both those imported and those in the current module.