Documentation

Lean.Elab.Attributes

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