@[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 : 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.Compiler.LCNF.Arg) : 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.Compiler.LCNF.Arg) : Lean.Compiler.LCNF.PP.M Lean.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 : Lean.Compiler.LCNF.LetValue) : 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.

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

Equations

• Lean.Compiler.LCNF.PP.getFunType ps type = Lean.Compiler.LCNF.instantiateForall type (Array.map (fun (x : Lean.Compiler.LCNF.Param) => Lean.mkFVar x.fvarId) ps)

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 (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 : 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.ppLetValue (e : Lean.Compiler.LCNF.LetValue) : Lean.Compiler.LCNF.CompilerM Lean.Format

Equations

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

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

• 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 : 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

• Lean.Compiler.LCNF.runCompilerWithoutModifyingState x = do let s ← get tryFinally (x.run { lctx := { params := ∅, letDecls := ∅, funDecls := ∅ }, nextIdx := 1 }) (set s)

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

• 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 : 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

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