source
def Lean.Compiler.LCNF.shouldGenerateCode (declName : Name) :
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.

Instances For

source
def Lean.Compiler.LCNF.checkpoint (stepName : Name) (decls : Array Decl) (shouldCheck : Bool) :
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.

Instances For

source
def Lean.Compiler.LCNF.isValidMainType (type : Expr) :
Bool
Equations

- One or more equations did not get rendered due to their size.
- Lean.Compiler.LCNF.isValidMainType (Lean.Expr.forallE binderName d b binderInfo) = false
- Lean.Compiler.LCNF.isValidMainType ((Lean.Expr.const `IO us).app (Lean.Expr.const resultName us_1)) = (fun (name : Lean.Name) => name == `UInt32 || name == `Unit || name == `PUnit) resultName
- Lean.Compiler.LCNF.isValidMainType type = false

Instances For

source
def Lean.Compiler.LCNF.PassManager.run (declNames : Array Name) :
CompilerM (Array IR.Decl)
Equations

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

Instances For

source
def Lean.Compiler.LCNF.compile (declNames : Array Name) :
CoreM (Array IR.Decl)
Equations

- Lean.Compiler.LCNF.compile declNames = (Lean.Compiler.LCNF.PassManager.run declNames).run

Instances For

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

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

Instances For

source
@[export lean_lcnf_compile_decls]
def Lean.Compiler.LCNF.main (declNames : Array Name) :
CoreM Unit
Equations

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

Instances For