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

A postponed call of compileDecls.

• declNames : Array Name

  Declaration names of this mutual group.

• options : Options

  Options at time of original call, to be restored for tracing etc.

@[implicit_reducible]

instance Lean.Compiler.LCNF.instBEqPostponedCompileDecls : BEq PostponedCompileDecls

Equations

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

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

Equations

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

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) (baseOpts : Options) : CoreM Unit

Equations

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

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

Equations

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

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

Equations

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