structure Lake.OrderedTagAttribute : Type

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

@[instance_reducible]

instance Lake.instInhabitedOrderedTagAttribute : Inhabited OrderedTagAttribute

Equations

• Lake.instInhabitedOrderedTagAttribute = { default := Lake.instInhabitedOrderedTagAttribute.default }

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

Equations

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

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

Equations

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

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.

Equations

• attr.getAllEntries env = Array.flatMap id (attr.ext.toEnvExtension.getState env).importedEntries ++ (attr.ext.toEnvExtension.getState env).state