@[reducible, 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 : FVarId) : M Format

Equations

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

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

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Compiler.LCNF.PP.ppArg Lean.Compiler.LCNF.Arg.erased = pure (Std.Format.text "◾")
• Lean.Compiler.LCNF.PP.ppArg (Lean.Compiler.LCNF.Arg.fvar fvarId) = Lean.Compiler.LCNF.PP.ppFVar fvarId

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

Equations

• Lean.Compiler.LCNF.PP.ppArgs args = Lean.Compiler.LCNF.PP.prefixJoin✝ (Std.Format.text " ") args Lean.Compiler.LCNF.PP.ppArg

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Compiler.LCNF.PP.ppLetValue Lean.Compiler.LCNF.LetValue.erased = pure (Std.Format.text "◾")
• Lean.Compiler.LCNF.PP.ppLetValue (Lean.Compiler.LCNF.LetValue.value v) = Lean.Compiler.LCNF.PP.ppExpr v.toExpr

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

Equations

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

def Lean.Compiler.LCNF.PP.ppParams (params : Array Param) : M 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 : LetDecl) : M Format

Equations

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

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

Equations

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

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

Equations

• Lean.Compiler.LCNF.PP.ppDeclValue (Lean.Compiler.LCNF.DeclValue.code c) = Lean.Compiler.LCNF.PP.ppCode c
• Lean.Compiler.LCNF.PP.ppDeclValue (Lean.Compiler.LCNF.DeclValue.extern externAttrData) = pure (Std.Format.text "extern")

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

Equations

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

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

Equations

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

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

Equations

• Lean.Compiler.LCNF.ppLetValue e = Lean.Compiler.LCNF.PP.run (Lean.Compiler.LCNF.PP.ppLetValue e)

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

Equations

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

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

Equations

• Lean.Compiler.LCNF.ppFunDecl decl = Lean.Compiler.LCNF.PP.run do let __do_lift ← Lean.Compiler.LCNF.PP.ppFunDecl decl pure (Std.format "fun " ++ Std.format __do_lift ++ Std.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.

Equations

• Lean.Compiler.LCNF.runCompilerWithoutModifyingState x = do let s ← get tryFinally x.run (set s)

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.

Equations

• Lean.Compiler.LCNF.ppDecl' decl = Lean.Compiler.LCNF.runCompilerWithoutModifyingState do let __do_lift ← decl.internalize Lean.Compiler.LCNF.ppDecl __do_lift

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.

Equations

• Lean.Compiler.LCNF.ppCode' code = Lean.Compiler.LCNF.runCompilerWithoutModifyingState do let __do_lift ← code.internalize Lean.Compiler.LCNF.ppCode __do_lift