Documentation

Lean.Compiler.LCNF.Main

source
def Lean.Compiler.LCNF.shouldGenerateCode (declName : Lean.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 [macroInline].
  • 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.
source
def Lean.Compiler.LCNF.shouldGenerateCode.isCompIrrelevant (declName : Lean.Name) :
Lean.MetaM Bool
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Compiler.LCNF.checkpoint (stepName : Lean.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.
source
def Lean.Compiler.LCNF.PassManager.run (declNames : Array Lean.Name) :
Lean.Compiler.LCNF.CompilerM (Array Lean.Compiler.LCNF.Decl)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Compiler.LCNF.compile (declNames : Array Lean.Name) :
Lean.CoreM (Array Lean.Compiler.LCNF.Decl)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Compiler.LCNF.showDecl (phase : Lean.Compiler.LCNF.Phase) (declName : Lean.Name) :
Lean.CoreM Lean.Format
Equations
  • One or more equations did not get rendered due to their size.
source
@[export lean_lcnf_compile_decls]
def Lean.Compiler.LCNF.main (declNames : List Lean.Name) :
Lean.CoreM Unit
Equations
  • One or more equations did not get rendered due to their size.