Documentation

Lean.Elab.Attributes

source
structure Lean.Elab.Attribute:
Type
source
instance Lean.Elab.instInhabitedAttribute:
Inhabited Lean.Elab.Attribute
Equations
source
instance Lean.Elab.instToFormatAttribute:
Lean.ToFormat Lean.Elab.Attribute
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.toAttributeKind (attrKindStx : Lean.Syntax) :
Lean.MacroM Lean.AttributeKind
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.mkAttrKindGlobal:
Lean.Syntax
Equations
source
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] (attrInstance : Lean.Syntax) :
m Lean.Elab.Attribute
Equations
  • One or more equations did not get rendered due to their size.
source
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] (attrInstances : Array Lean.Syntax) :
m (Array Lean.Elab.Attribute)
Equations
  • One or more equations did not get rendered due to their size.
source
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] (stx : Lean.Syntax) :
m (Array Lean.Elab.Attribute)
Equations