# 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.
Equations
• One or more equations did not get rendered due to their size.
def Lean.Compiler.LCNF.checkpoint (stepName : Lean.Name) (decls : ) :

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.
Equations
• One or more equations did not get rendered due to their size.
def Lean.Compiler.LCNF.compile (declNames : ) :
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
@[export lean_lcnf_compile_decls]
def Lean.Compiler.LCNF.main (declNames : ) :
Equations
• One or more equations did not get rendered due to their size.