structure Lean.Elab.Attribute : Type

• kind : Lean.AttributeKind
• name : Lake.Name
• stx : Lean.Syntax

instance Lean.Elab.instInhabitedAttribute : Inhabited Lean.Elab.Attribute

Equations

• Lean.Elab.instInhabitedAttribute = { default := { kind := default, name := default, stx := default } }

instance Lean.Elab.instToFormatAttribute : Lean.ToFormat Lean.Elab.Attribute

Equations

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

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

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

Equations

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

def Lean.Elab.mkAttrKindGlobal : Lean.Syntax

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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