structure Lean.Compiler.LCNF.ConfigOptions : Type

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

  smallThreshold : Nat

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

  maxRecInline : Nat

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

  maxRecInlineIfReduce : Nat

• Perform type compatibility checking after each compiler pass.

  checkTypes : Bool

User controlled configuration options for the code generator.

instance Lean.Compiler.LCNF.instInhabitedConfigOptions : Inhabited Lean.Compiler.LCNF.ConfigOptions

Equations

• Lean.Compiler.LCNF.instInhabitedConfigOptions = { default := { smallThreshold := default, maxRecInline := default, maxRecInlineIfReduce := default, checkTypes := 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

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

Equations

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