Documentation

Lean.Compiler.LCNF.ConfigOptions

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

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