ORM attributes

@[typedb "label"] on a structure sets its TypeDB type label (default: the kebab-case of the type's name). Field-level settings are type markers (Key, Role, Label in TypeDB.ORM), because Lean does not accept attributes on structure fields.

def TypeDB.ORM.typedb : Lean.ParserDescr

Equations

• TypeDB.ORM.typedb = Lean.ParserDescr.node `TypeDB.ORM.typedb 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "typedb " false) (Lean.ParserDescr.const `str))

opaque TypeDB.ORM.typedbLabelAttr : Lean.ParametricAttribute String