Documentation

Lean.Compiler.InlineAttrs

inductive Lean.Compiler.InlineAttributeKind :

inline: Lean.Compiler.InlineAttributeKind
noinline: Lean.Compiler.InlineAttributeKind
macroInline: Lean.Compiler.InlineAttributeKind
inlineIfReduce: Lean.Compiler.InlineAttributeKind
alwaysInline: Lean.Compiler.InlineAttributeKind

Instances For

instance Lean.Compiler.instInhabitedInlineAttributeKind :

Inhabited Lean.Compiler.InlineAttributeKind

Equations

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

instance Lean.Compiler.instBEqInlineAttributeKind :

BEq Lean.Compiler.InlineAttributeKind

Equations

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

instance Lean.Compiler.instHashableInlineAttributeKind :

Hashable Lean.Compiler.InlineAttributeKind

Equations

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

opaque Lean.Compiler.inlineAttrs :

Lean.EnumAttributes Lean.Compiler.InlineAttributeKind

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

Except String Lean.Environment

Equations

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

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

Option Lean.Compiler.InlineAttributeKind

Equations

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

@[reducible, inline]

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

@[reducible, inline]

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

Equations

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

@[export lean_has_inline_attribute]

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

Equations

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

@[export lean_has_inline_if_reduce_attribute]

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

Equations

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

@[export lean_has_noinline_attribute]

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

Equations

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

@[export lean_has_macro_inline_attribute]

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

Equations

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