Documentation

Lean.Compiler.LCNF.PrettyPrinter

source
@[inline]
abbrev Lean.Compiler.LCNF.PP.M (α : Type) :
Type
Equations
source
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.
source
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.
source
def Lean.Compiler.LCNF.PP.ppArg (e : Lean.Compiler.LCNF.Arg) :
Lean.Compiler.LCNF.PP.M Lean.Format
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Compiler.LCNF.PP.ppArgs (args : Array Lean.Compiler.LCNF.Arg) :
Lean.Compiler.LCNF.PP.M Lean.Format
Equations
source
def Lean.Compiler.LCNF.PP.ppLetValue (e : Lean.Compiler.LCNF.LetValue) :
Lean.Compiler.LCNF.PP.M Lean.Format
Equations
  • One or more equations did not get rendered due to their size.
source
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.
source
def Lean.Compiler.LCNF.PP.ppParams (params : Array Lean.Compiler.LCNF.Param) :
Lean.Compiler.LCNF.PP.M Lean.Format
Equations
source
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.
source
def Lean.Compiler.LCNF.PP.getFunType (ps : Array Lean.Compiler.LCNF.Param) (type : Lean.Expr) :
Lean.CoreM Lean.Expr
Equations
source
partial def Lean.Compiler.LCNF.PP.ppFunDecl (funDecl : Lean.Compiler.LCNF.FunDecl) :
Lean.Compiler.LCNF.PP.M Lean.Format
source
partial def Lean.Compiler.LCNF.PP.ppAlt (alt : Lean.Compiler.LCNF.Alt) :
Lean.Compiler.LCNF.PP.M Lean.Format
source
partial def Lean.Compiler.LCNF.PP.ppCode (c : Lean.Compiler.LCNF.Code) :
Lean.Compiler.LCNF.PP.M Lean.Format
source
def Lean.Compiler.LCNF.PP.run {α : Type} (x : Lean.Compiler.LCNF.PP.M α) :
Lean.Compiler.LCNF.CompilerM α
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Compiler.LCNF.ppCode (code : Lean.Compiler.LCNF.Code) :
Lean.Compiler.LCNF.CompilerM Lean.Format
Equations
source
def Lean.Compiler.LCNF.ppLetValue (e : Lean.Compiler.LCNF.LetValue) :
Lean.Compiler.LCNF.CompilerM Lean.Format
Equations
source
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.
source
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.
source
def Lean.Compiler.LCNF.runCompilerWithoutModifyingState {α : Type} (x : Lean.Compiler.LCNF.CompilerM α) :
Lean.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.

Equations
  • One or more equations did not get rendered due to their size.
source
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
source
def Lean.Compiler.LCNF.ppCode' (code : Lean.Compiler.LCNF.Code) :
Lean.CoreM Lean.Format

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

Equations