Documentation

Lean.Elab.Attributes

source
structure Lean.Elab.Attribute :
Type
Instances For
    source
    @[instance_reducible]
    instance Lean.Elab.instInhabitedAttribute :
    Inhabited Attribute
    source
    @[instance_reducible]
    instance Lean.Elab.instToFormatAttribute :
    ToFormat Attribute
    source
    def Lean.Elab.toAttributeKind (attrKindStx : Syntax) :
    MacroM AttributeKind
    attrKind := leading_parser optional («scoped» <|> «local»)
    Instances For
      source
      def Lean.Elab.mkAttrKindGlobal :
      Syntax
      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] [MonadFinally m] (attrInstance : Syntax) :
        m Attribute
        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] [MonadFinally m] (attrInstances : Array Syntax) :
          m (Array Attribute)
          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] [MonadFinally m] (stx : Syntax) :
            m (Array Attribute)
            Instances For