@[reducible, inline]

abbrev Lean.Compiler.LCNF.PP.M (α : Type) : Type

def Lean.Compiler.LCNF.PP.ppFVar (fvarId : FVarId) : M Format

def Lean.Compiler.LCNF.PP.ppExpr (e : Expr) : M Format

def Lean.Compiler.LCNF.PP.ppArg (e : Arg) : M Format

def Lean.Compiler.LCNF.PP.ppArgs (args : Array Arg) : M Format

def Lean.Compiler.LCNF.PP.ppLitValue (lit : LitValue) : M Format

def Lean.Compiler.LCNF.PP.ppLetValue (e : LetValue) : M Format

def Lean.Compiler.LCNF.PP.ppParam (param : Param) : M Format

def Lean.Compiler.LCNF.PP.ppParams (params : Array Param) : M Format

def Lean.Compiler.LCNF.PP.ppLetDecl (letDecl : LetDecl) : M Format

def Lean.Compiler.LCNF.PP.getFunType (ps : Array Param) (type : Expr) : CoreM Expr

partial def Lean.Compiler.LCNF.PP.ppFunDecl (funDecl : FunDecl) : M Format

partial def Lean.Compiler.LCNF.PP.ppAlt (alt : Alt) : M Format

partial def Lean.Compiler.LCNF.PP.ppCode (c : Code) : M Format

def Lean.Compiler.LCNF.PP.ppDeclValue (b : DeclValue) : M Format

def Lean.Compiler.LCNF.PP.run {α : Type} (x : M α) : CompilerM α

def Lean.Compiler.LCNF.ppCode (code : Code) : CompilerM Format

def Lean.Compiler.LCNF.ppLetValue (e : LetValue) : CompilerM Format

def Lean.Compiler.LCNF.ppDecl (decl : Decl) : CompilerM Format

def Lean.Compiler.LCNF.ppFunDecl (decl : FunDecl) : CompilerM Format

def Lean.Compiler.LCNF.runCompilerWithoutModifyingState {α : Type} (x : CompilerM α) : CoreM α

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.

def Lean.Compiler.LCNF.ppDecl' (decl : Decl) : CoreM Format

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

def Lean.Compiler.LCNF.ppCode' (code : Code) : CoreM Format

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