Documentation

Lean.Elab.Attributes

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