structure Lean.Elab.Attribute : Type

• kind : AttributeKind
• name : Name
• stx : Syntax

@[instance_reducible]

instance Lean.Elab.instInhabitedAttribute : Inhabited Attribute

Equations

• Lean.Elab.instInhabitedAttribute = { default := Lean.Elab.instInhabitedAttribute.default }

@[instance_reducible]

instance Lean.Elab.instToFormatAttribute : ToFormat Attribute

Equations

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

def Lean.Elab.toAttributeKind (attrKindStx : Syntax) : MacroM AttributeKind

attrKind := leading_parser optional («scoped» <|> «local»)

Equations

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

def Lean.Elab.mkAttrKindGlobal : Syntax

Equations

• Lean.Elab.mkAttrKindGlobal = (Lean.mkNode `Lean.Parser.Term.attrKind #[Lean.mkNullNode]).raw

def Lean.Elab.elabAttr {m : Type → Type} [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLiftT IO m] [MonadFinally m] (attrInstance : Syntax) : m Attribute

Equations

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

def Lean.Elab.elabAttrs {m : Type → Type} [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadLiftT IO m] [MonadFinally m] (attrInstances : Array Syntax) : m (Array Attribute)

Equations

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

def Lean.Elab.elabDeclAttrs {m : Type → Type} [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadLiftT IO m] [MonadFinally m] (stx : Syntax) : m (Array Attribute)

Equations

• Lean.Elab.elabDeclAttrs stx = Lean.Elab.elabAttrs stx[1].getSepArgs