inductive Lean.Compiler.InlineAttributeKind : Type

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

instance Lean.Compiler.instInhabitedInlineAttributeKind : Inhabited InlineAttributeKind

instance Lean.Compiler.instBEqInlineAttributeKind : BEq InlineAttributeKind

instance Lean.Compiler.instHashableInlineAttributeKind : Hashable InlineAttributeKind

opaque Lean.Compiler.inlineAttrs : EnumAttributes InlineAttributeKind

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

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

@[reducible, inline]

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

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

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

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

@[reducible, inline]

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

@[export lean_has_inline_attribute]

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

@[export lean_has_inline_if_reduce_attribute]

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

@[export lean_has_noinline_attribute]

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

@[export lean_has_macro_inline_attribute]

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