Documentation

Lean.Compiler.InlineAttrs

source
inductive Lean.Compiler.InlineAttributeKind :
Type
Instances For
    source
    instance Lean.Compiler.instInhabitedInlineAttributeKind :
    Inhabited InlineAttributeKind
    Equations
    source
    instance Lean.Compiler.instBEqInlineAttributeKind :
    BEq InlineAttributeKind
    Equations
    source
    instance Lean.Compiler.instHashableInlineAttributeKind :
    Hashable InlineAttributeKind
    Equations
    source
    opaque Lean.Compiler.inlineAttrs :
    EnumAttributes InlineAttributeKind
    source
    def Lean.Compiler.setInlineAttribute (env : Environment) (declName : Name) (kind : InlineAttributeKind) :
    Except String Environment
    Equations
    Instances For
      source
      def Lean.Compiler.getInlineAttribute? (env : Environment) (declName : Name) :
      Option InlineAttributeKind
      Equations
      Instances For
        source
        @[reducible, inline]
        abbrev Lean.Compiler.hasInlineAttribute (env : Environment) (declName : Name) :
        Bool
        Equations
        Instances For
          source
          def Lean.Compiler.hasInlineIfReduceAttribute (env : Environment) (declName : Name) :
          Bool
          Equations
          Instances For
            source
            def Lean.Compiler.hasNoInlineAttribute (env : Environment) (declName : Name) :
            Bool
            Equations
            Instances For
              source
              def Lean.Compiler.hasMacroInlineAttribute (env : Environment) (declName : Name) :
              Bool
              Equations
              Instances For
                source
                @[reducible, inline]
                abbrev Lean.Compiler.hasAlwaysInlineAttribute (env : Environment) (declName : Name) :
                Bool
                Equations
                Instances For
                  source
                  @[export lean_has_inline_attribute]
                  def Lean.Compiler.hasInlineAttributeOld (env : Environment) (n : Name) :
                  Bool
                  Equations
                  Instances For
                    source
                    @[export lean_has_inline_if_reduce_attribute]
                    def Lean.Compiler.hasInlineIfReduceAttributeOld (env : Environment) (n : Name) :
                    Bool
                    Equations
                    Instances For
                      source
                      @[export lean_has_noinline_attribute]
                      def Lean.Compiler.hasNoInlineAttributeOld (env : Environment) (n : Name) :
                      Bool
                      Equations
                      Instances For
                        source
                        @[export lean_has_macro_inline_attribute]
                        def Lean.Compiler.hasMacroInlineAttributeOld (env : Environment) (n : Name) :
                        Bool
                        Equations
                        Instances For