@[inline]

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

Equations

• Lean.Compiler.LCNF.PP.M = ReaderT Lean.LocalContext Lean.Compiler.LCNF.CompilerM

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lean.Compiler.LCNF.PP.ppArgs args = Lean.Compiler.LCNF.PP.join args Lean.Compiler.LCNF.PP.ppArg

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lean.Compiler.LCNF.PP.ppParams params = Lean.Compiler.LCNF.PP.prefixJoin (Std.Format.text " ") params Lean.Compiler.LCNF.PP.ppParam

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

Equations

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

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

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

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

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

Equations

• Lean.Compiler.LCNF.PP.run x = Lean.withOptions (fun a => Lean.Option.set a Lean.pp.sanitizeNames false) do let a ← get ReaderT.run x (Lean.Compiler.LCNF.LCtx.toLocalContext a.lctx)

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

Equations

• Lean.Compiler.LCNF.ppCode code = Lean.Compiler.LCNF.PP.run (Lean.Compiler.LCNF.PP.ppCode code)

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

Equations

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

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

Equations

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

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

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

This function is used for debugging purposes.

Equations

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

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

Equations

• Lean.Compiler.LCNF.ppDecl'.go decl = do let decl ← Lean.Compiler.LCNF.Decl.internalize decl ∅ Lean.Compiler.LCNF.ppDecl decl