structure Lake.OrderedTagAttribute : Type

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

instance Lake.instInhabitedOrderedTagAttribute : Inhabited Lake.OrderedTagAttribute

def Lake.registerOrderedTagAttribute (name : Lake.Name) (descr : String) (validate : optParam (Lake.Name → Lean.AttrM Unit) fun x => pure ()) (ref : autoParam Lake.Name _auto✝) : IO Lake.OrderedTagAttribute

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