partial def Lean.Compiler.LCNF.markDeclPublicRec {pu : Purity} (phase : Phase) (decl : Decl pu) : 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.

opaque Lean.Compiler.LCNF.compiler.relaxedMetaCheck : Lean.Option Bool

def Lean.Compiler.LCNF.checkMeta {pu : Purity} (origDecl : Decl pu) : CompilerM Unit

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

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.

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