Documentation

Lean.Compiler.InlineAttrs

source
inductive Lean.Compiler.InlineAttributeKind :
Type
source
instance Lean.Compiler.instBEqInlineAttributeKind :
BEq Lean.Compiler.InlineAttributeKind
Equations
source
instance Lean.Compiler.instInhabitedInlineAttributeKind :
Inhabited Lean.Compiler.InlineAttributeKind
Equations
source
constant Lean.Compiler.inlineAttrs :
Lean.EnumAttributes Lean.Compiler.InlineAttributeKind
source
def Lean.Compiler.hasInlineAttribute (env : Lean.Environment) (n : Lean.Name) :
Bool
Equations
source
def Lean.Compiler.hasInlineIfReduceAttribute (env : Lean.Environment) (n : Lean.Name) :
Bool
Equations
source
def Lean.Compiler.hasNoInlineAttribute (env : Lean.Environment) (n : Lean.Name) :
Bool
Equations
source
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