Documentation

Lean.Compiler.InlineAttrs

source
inductive Lean.Compiler.InlineAttributeKind :
Type
Instances For
    source
    instance Lean.Compiler.instInhabitedInlineAttributeKind :
    Inhabited InlineAttributeKind
    Equations
    source
    def Lean.Compiler.instInhabitedInlineAttributeKind.default :
    InlineAttributeKind
    Equations
    Instances For
      source
      def Lean.Compiler.instBEqInlineAttributeKind.beq :
      InlineAttributeKind → InlineAttributeKind → Bool
      Equations
      Instances For
        source
        instance Lean.Compiler.instBEqInlineAttributeKind :
        BEq InlineAttributeKind
        Equations
        source
        def Lean.Compiler.instHashableInlineAttributeKind.hash :
        InlineAttributeKind → UInt64
        Equations
        Instances For
          source
          instance Lean.Compiler.instHashableInlineAttributeKind :
          Hashable InlineAttributeKind
          Equations
          source
          opaque Lean.Compiler.inlineAttrs :
          EnumAttributes InlineAttributeKind

          Changes the inlining behavior. This attribute comes in several variants:

          • @[inline]: marks the definition to be inlined when it is appropriate.
          • @[inline_if_reduce]: marks the definition to be inlined if an application of it after inlining and applying reduction isn't a match expression. This attribute can be used for inlining structurally recursive functions.
          • @[noinline]: marks the definition to never be inlined.
          • @[always_inline]: marks the definition to always be inlined.
          • @[macro_inline]: marks the definition to always be inlined at the beginning of compilation. This makes it possible to define functions that evaluate some of their parameters lazily. Example:
            @[macro_inline]
def test (x y : Nat) : Nat :=
  if x = 42 then x else y

#eval test 42 (2^1000000000000) -- doesn't compute 2^1000000000000
            Only non-recursive functions may be marked @[macro_inline].
          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
              @[inline]
              def 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
                      @[inline]
                      def Lean.Compiler.hasAlwaysInlineAttribute (env : Environment) (declName : Name) :
                      Bool
                      Equations
                      Instances For