# Documentation

Lean.Compiler.LCNF.ConfigOptions

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

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