Documentation

Lean.Compiler.InlineAttrs

inductive Lean.Compiler.InlineAttributeKind :

inline : InlineAttributeKind
noinline : InlineAttributeKind
macroInline : InlineAttributeKind
inlineIfReduce : InlineAttributeKind
alwaysInline : InlineAttributeKind

Instances For

instance Lean.Compiler.instInhabitedInlineAttributeKind :

Inhabited InlineAttributeKind

Equations

Lean.Compiler.instInhabitedInlineAttributeKind = { default := Lean.Compiler.InlineAttributeKind.inline }

instance Lean.Compiler.instBEqInlineAttributeKind :

BEq InlineAttributeKind

Equations

Lean.Compiler.instBEqInlineAttributeKind = { beq := Lean.Compiler.beqInlineAttributeKind✝ }

instance Lean.Compiler.instHashableInlineAttributeKind :

Hashable InlineAttributeKind

Equations

Lean.Compiler.instHashableInlineAttributeKind = { hash := Lean.Compiler.hashInlineAttributeKind✝ }

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].

def Lean.Compiler.setInlineAttribute (env : Environment) (declName : Name) (kind : InlineAttributeKind) :

Except String Environment

Equations

Lean.Compiler.setInlineAttribute env declName kind = Lean.Compiler.inlineAttrs.setValue env declName kind

Instances For

def Lean.Compiler.getInlineAttribute? (env : Environment) (declName : Name) :

Option InlineAttributeKind

Equations

Lean.Compiler.getInlineAttribute? env declName = Lean.Compiler.inlineAttrs.getValue env declName

Instances For

@[reducible, inline]

abbrev Lean.Compiler.hasInlineAttribute (env : Environment) (declName : Name) :

Equations

Lean.Compiler.hasInlineAttribute env declName = Lean.Compiler.hasInlineAttrCore✝ env Lean.Compiler.InlineAttributeKind.inline declName

Instances For

def Lean.Compiler.hasInlineIfReduceAttribute (env : Environment) (declName : Name) :

Equations

Lean.Compiler.hasInlineIfReduceAttribute env declName = Lean.Compiler.hasInlineAttrCore✝ env Lean.Compiler.InlineAttributeKind.inlineIfReduce declName

Instances For

def Lean.Compiler.hasNoInlineAttribute (env : Environment) (declName : Name) :

Equations

Lean.Compiler.hasNoInlineAttribute env declName = Lean.Compiler.hasInlineAttrCore✝ env Lean.Compiler.InlineAttributeKind.noinline declName

Instances For

def Lean.Compiler.hasMacroInlineAttribute (env : Environment) (declName : Name) :

Equations

Lean.Compiler.hasMacroInlineAttribute env declName = Lean.Compiler.hasInlineAttrCore✝ env Lean.Compiler.InlineAttributeKind.macroInline declName

Instances For

@[reducible, inline]

abbrev Lean.Compiler.hasAlwaysInlineAttribute (env : Environment) (declName : Name) :

Equations

Lean.Compiler.hasAlwaysInlineAttribute env declName = Lean.Compiler.hasInlineAttrCore✝ env Lean.Compiler.InlineAttributeKind.alwaysInline declName

Instances For

@[export lean_has_inline_attribute]

def Lean.Compiler.hasInlineAttributeOld (env : Environment) (n : Name) :

Equations

Lean.Compiler.hasInlineAttributeOld env n = Lean.Compiler.hasInlineAttrAux✝ env Lean.Compiler.InlineAttributeKind.inline n

Instances For

@[export lean_has_inline_if_reduce_attribute]

def Lean.Compiler.hasInlineIfReduceAttributeOld (env : Environment) (n : Name) :

Equations

Lean.Compiler.hasInlineIfReduceAttributeOld env n = Lean.Compiler.hasInlineAttrAux✝ env Lean.Compiler.InlineAttributeKind.inlineIfReduce n

Instances For

@[export lean_has_noinline_attribute]

def Lean.Compiler.hasNoInlineAttributeOld (env : Environment) (n : Name) :

Equations

Lean.Compiler.hasNoInlineAttributeOld env n = Lean.Compiler.hasInlineAttrAux✝ env Lean.Compiler.InlineAttributeKind.noinline n

Instances For

@[export lean_has_macro_inline_attribute]

def Lean.Compiler.hasMacroInlineAttributeOld (env : Environment) (n : Name) :

Equations

Lean.Compiler.hasMacroInlineAttributeOld env n = Lean.Compiler.hasInlineAttrAux✝ env Lean.Compiler.InlineAttributeKind.macroInline n

Instances For