source
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.

Instances For

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

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

Instances For

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

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

source
opaque Lean.Compiler.LCNF.compiler.small :
Lean.Option Nat
source
opaque Lean.Compiler.LCNF.compiler.maxRecInline :
Lean.Option Nat
source
opaque Lean.Compiler.LCNF.compiler.maxRecInlineIfReduce :
Lean.Option Nat
source
opaque Lean.Compiler.LCNF.compiler.checkTypes :
Lean.Option Bool
source
opaque Lean.Compiler.LCNF.compiler.extract_closed :
Lean.Option Bool
source
def Lean.Compiler.LCNF.toConfigOptions (opts : Options) :
ConfigOptions
Equations

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

Instances For