structure Lean.Compiler.LCNF.ConfigOptions : Type

User controlled configuration options for the code generator.

• smallThreshold : Nat

  Any function declaration or join point with size ≤ smallThreshold is inlined even if there are multiple occurrences.

• maxRecInline : Nat

  Maximum number of times a recursive definition tagged with [inline] can be recursively inlined before generating an error during compilation.

• maxRecInlineIfReduce : Nat

  Maximum number of times a recursive definition tagged with [inline_if_reduce] can be recursively inlined before generating an error during compilation.

• checkTypes : Bool

  Perform type compatibility checking after each compiler pass.

• extractClosed : Bool

  Cache closed terms and evaluate them at initialization time.

def Lean.Compiler.LCNF.instInhabitedConfigOptions.default : ConfigOptions

Equations

• Lean.Compiler.LCNF.instInhabitedConfigOptions.default = { smallThreshold := default, maxRecInline := default, maxRecInlineIfReduce := default, checkTypes := default, extractClosed := default }

instance Lean.Compiler.LCNF.instInhabitedConfigOptions : Inhabited ConfigOptions

Equations

• Lean.Compiler.LCNF.instInhabitedConfigOptions = { default := Lean.Compiler.LCNF.instInhabitedConfigOptions.default }

opaque Lean.Compiler.LCNF.compiler.small : Lean.Option Nat

opaque Lean.Compiler.LCNF.compiler.maxRecInline : Lean.Option Nat

opaque Lean.Compiler.LCNF.compiler.maxRecInlineIfReduce : Lean.Option Nat

opaque Lean.Compiler.LCNF.compiler.checkTypes : Lean.Option Bool

opaque Lean.Compiler.LCNF.compiler.extract_closed : Lean.Option Bool

def Lean.Compiler.LCNF.toConfigOptions (opts : Options) : ConfigOptions

Equations

• One or more equations did not get rendered due to their size.