structure Lean.Elab.Attribute : Type

• kind : Lean.AttributeKind
• name : Lean.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} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadResolveName m] [inst : Lean.MonadError m] [inst : Lean.Elab.MonadMacroAdapter m] [inst : Lean.MonadRecDepth m] [inst : Lean.MonadTrace m] [inst : Lean.MonadOptions m] [inst : Lean.AddMessageContext m] [inst : Lean.Elab.MonadInfoTree m] [inst : 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} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadResolveName m] [inst : Lean.MonadError m] [inst : Lean.Elab.MonadMacroAdapter m] [inst : Lean.MonadRecDepth m] [inst : Lean.MonadTrace m] [inst : Lean.MonadOptions m] [inst : Lean.AddMessageContext m] [inst : Lean.MonadLog m] [inst : Lean.Elab.MonadInfoTree m] [inst : 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} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadResolveName m] [inst : Lean.MonadError m] [inst : Lean.Elab.MonadMacroAdapter m] [inst : Lean.MonadRecDepth m] [inst : Lean.MonadTrace m] [inst : Lean.MonadOptions m] [inst : Lean.AddMessageContext m] [inst : Lean.MonadLog m] [inst : Lean.Elab.MonadInfoTree m] [inst : MonadLiftT IO m] (stx : Lean.Syntax) : m (Array Lean.Elab.Attribute)

Equations

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