Documentation

Lean.Compiler.LCNF.Main

We do not generate code for declName if

  • Its type is a proposition.
  • Its type is a type former.
  • It is tagged as [macro_inline].
  • It is a type class instance.

Remark: we still generate code for declarations tagged as [inline] and [specialize] since they can be partially applied.

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

      A checkpoint in code generation to print all declarations in between compiler passes in order to ease debugging. The trace can be viewed with set_option trace.Compiler.step true.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          Equations
          Instances For
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[export lean_lcnf_compile_decls]
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For