structure Lean.Compiler.LCNF.ConfigOptions : Type

• smallThreshold : Nat

  Any function declaration or join point with size ≤ smallThresold 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.

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.