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.

def Lean.Compiler.LCNF.checkpoint {pu : Purity} (stepName : Name) (decls : Array (Decl pu)) (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.

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

structure Lean.Compiler.LCNF.PostponedCompileDecls : Type

• declNames : Array Name

def Lean.Compiler.LCNF.instBEqPostponedCompileDecls.beq : PostponedCompileDecls → PostponedCompileDecls → Bool

Equations

• Lean.Compiler.LCNF.instBEqPostponedCompileDecls.beq { declNames := a } { declNames := b } = (a == b)
• Lean.Compiler.LCNF.instBEqPostponedCompileDecls.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Lean.Compiler.LCNF.instBEqPostponedCompileDecls : BEq PostponedCompileDecls

Equations

• Lean.Compiler.LCNF.instBEqPostponedCompileDecls = { beq := Lean.Compiler.LCNF.instBEqPostponedCompileDecls.beq }

def Lean.Compiler.LCNF.instHashablePostponedCompileDecls.hash : PostponedCompileDecls → UInt64

Equations

• Lean.Compiler.LCNF.instHashablePostponedCompileDecls.hash { declNames := a } = mixHash 0 (hash a)

@[implicit_reducible]

instance Lean.Compiler.LCNF.instHashablePostponedCompileDecls : Hashable PostponedCompileDecls

Equations

• Lean.Compiler.LCNF.instHashablePostponedCompileDecls = { hash := Lean.Compiler.LCNF.instHashablePostponedCompileDecls.hash }

opaque Lean.Compiler.LCNF.postponedCompileDeclsExt : SimplePersistentEnvExtension PostponedCompileDecls (NameMap PostponedCompileDecls)

Saves postponed compileDecls calls.

We use this state both in lean when doing post-hoc compilation of non-meta declarations on #eval etc. as well as in leanir to do separate compilation of all defs.

def Lean.Compiler.LCNF.resumeCompilation (declName : Name) : CoreM Unit

Equations

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

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

Equations

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

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

Equations

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