def Lean.Compiler.LCNF.shouldGenerateCode (declName : Lake.Name) : Lean.CoreM Bool

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.

def Lean.Compiler.LCNF.shouldGenerateCode.isCompIrrelevant (declName : Lake.Name) : Lean.MetaM Bool

Equations

• Lean.Compiler.LCNF.shouldGenerateCode.isCompIrrelevant declName = do let info ← Lean.getConstInfo declName Lean.Meta.isProp info.type <||> Lean.Meta.isTypeFormerType info.type

def Lean.Compiler.LCNF.checkpoint (stepName : Lake.Name) (decls : Array Lean.Compiler.LCNF.Decl) : Lean.Compiler.LCNF.CompilerM Unit

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.

def Lean.Compiler.LCNF.PassManager.run (declNames : Array Lake.Name) : Lean.Compiler.LCNF.CompilerM (Array Lean.Compiler.LCNF.Decl)

Equations

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

def Lean.Compiler.LCNF.compile (declNames : Array Lake.Name) : Lean.CoreM (Array Lean.Compiler.LCNF.Decl)

Equations

• Lean.Compiler.LCNF.compile declNames = (Lean.Compiler.LCNF.PassManager.run declNames).run { lctx := { params := ∅, letDecls := ∅, funDecls := ∅ }, nextIdx := 1 }

def Lean.Compiler.LCNF.showDecl (phase : Lean.Compiler.LCNF.Phase) (declName : Lake.Name) : Lean.CoreM Lean.Format

Equations

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

@[export lean_lcnf_compile_decls]

def Lean.Compiler.LCNF.main (declNames : List Lake.Name) : Lean.CoreM Unit

Equations

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