Documentation

Lean.Compiler.InlineAttrs

source
inductive Lean.Compiler.InlineAttributeKind:
Type
source
instance Lean.Compiler.instInhabitedInlineAttributeKind:
Inhabited Lean.Compiler.InlineAttributeKind
Equations
source
instance Lean.Compiler.instBEqInlineAttributeKind:
BEq Lean.Compiler.InlineAttributeKind
Equations
source
opaque Lean.Compiler.inlineAttrs:
Lean.EnumAttributes Lean.Compiler.InlineAttributeKind
source
@[export lean_has_inline_attribute]
def Lean.Compiler.hasInlineAttribute (env : Lean.Environment) (n : Lean.Name) :
Bool
Equations
source
@[export lean_has_inline_if_reduce_attribute]
def Lean.Compiler.hasInlineIfReduceAttribute (env : Lean.Environment) (n : Lean.Name) :
Bool
Equations
source
@[export lean_has_noinline_attribute]
def Lean.Compiler.hasNoInlineAttribute (env : Lean.Environment) (n : Lean.Name) :
Bool
Equations
source
@[export lean_has_macro_inline_attribute]
def Lean.Compiler.hasMacroInlineAttribute (env : Lean.Environment) (n : Lean.Name) :
Bool
Equations
source
def Lean.Compiler.setInlineAttribute (env : Lean.Environment) (declName : Lean.Name) (kind : Lean.Compiler.InlineAttributeKind) :
Except String Lean.Environment
Equations