inductive Lean.Compiler.InlineAttributeKind : Type

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

instance Lean.Compiler.instInhabitedInlineAttributeKind : Inhabited Lean.Compiler.InlineAttributeKind

instance Lean.Compiler.instBEqInlineAttributeKind : BEq Lean.Compiler.InlineAttributeKind

instance Lean.Compiler.instHashableInlineAttributeKind : Hashable Lean.Compiler.InlineAttributeKind

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

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

@[inline, reducible]

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

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

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

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

@[inline, reducible]

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

@[export lean_has_inline_attribute]

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

@[export lean_has_inline_if_reduce_attribute]

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

@[export lean_has_noinline_attribute]

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

@[export lean_has_macro_inline_attribute]

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