# Documentation

Lean.Compiler.LCNF.PrettyPrinter

@[inline]
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
def Lean.Compiler.LCNF.PP.run {α : Type} (x : ) :
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.

Execute x in CoreM without modifying Cores state. This is useful if we want make sure we do not affect the next free variable id.

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

Similar to ppDecl, but in CoreM, and it does not assume decl has already been internalized. This function is used for debugging purposes.

Equations

Similar to ppCode, but in CoreM, and it does not assume code has already been internalized.

Equations