partial def Lean.Compiler.LCNF.markDeclPublicRec (phase : Phase) (decl : Decl) : CompilerM Unit

Marks the given declaration as to be exported and recursively infers the correct visibility of its body and referenced declarations based on that.

def Lean.Compiler.LCNF.checkMeta (origDecl : Decl) : CompilerM Unit

Checks whether references in the given declaration adhere to phase distinction.

Equations

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

def Lean.Compiler.LCNF.checkTemplateVisibility : Pass

Checks that imports necessary for inlining/specialization are public as otherwise we may run into unknown declarations at the point of inlining/specializing. This is a limitation that we want to lift in the future by moving main compilation into a different process that can use a different import/incremental system.

Equations

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

def Lean.Compiler.LCNF.inferVisibility (phase : Phase) : Pass

Equations

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