structure Lake.OrderedTagAttribute : Type

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

Instances For

• Lake.instInhabitedOrderedTagAttribute

instance Lake.instInhabitedOrderedTagAttribute : Inhabited Lake.OrderedTagAttribute

Equations

• Lake.instInhabitedOrderedTagAttribute = { default := { attr := default, ext := default } }

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

Equations

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

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

Equations

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

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

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

Equations

• attr.getAllEntries env = let s := attr.ext.toEnvExtension.getState env; Array.concatMap id s.importedEntries ++ s.state