source
structure Lean.Elab.Attribute :
Type

- kind : AttributeKind
- name : Name
- stx : Syntax

Instances For

source
def Lean.Elab.instInhabitedAttribute.default :
Attribute
Equations

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

Instances For

source
instance Lean.Elab.instInhabitedAttribute :
Inhabited Attribute
Equations

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

source
instance Lean.Elab.instToFormatAttribute :
ToFormat Attribute
Equations

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

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

Instances For

source
def Lean.Elab.mkAttrKindGlobal :
Syntax
Equations

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

Instances For

source
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] (attrInstance : Syntax) :
m Attribute
Equations

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

Instances For

source
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] (attrInstances : Array Syntax) :
m (Array Attribute)
Equations

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

Instances For

source
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] (stx : Syntax) :
m (Array Attribute)
Equations

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

Instances For