source
structure Lake.OrderedTagAttribute :
Type

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

Instances For

source
instance Lake.instInhabitedOrderedTagAttribute :
Inhabited OrderedTagAttribute
Equations

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

source
def Lake.instInhabitedOrderedTagAttribute.default :
OrderedTagAttribute
Equations

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

Instances For

source
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.

Instances For

source
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.

Instances For

source
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

Instances For