Documentation

Lean.Compiler.LCNF.Visibility

source
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.

source
def Lean.Compiler.LCNF.inferVisibility (phase : Phase) :
Pass
Equations
  • One or more equations did not get rendered due to their size.
Instances For