structure Lean.Compiler.LCNF.LCtx : Type

LCNF local context.

• params : Std.HashMap FVarId Param
• letDecls : Std.HashMap FVarId LetDecl
• funDecls : Std.HashMap FVarId FunDecl

instance Lean.Compiler.LCNF.instInhabitedLCtx : Inhabited LCtx

def Lean.Compiler.LCNF.LCtx.addParam (lctx : LCtx) (param : Param) : LCtx

def Lean.Compiler.LCNF.LCtx.addLetDecl (lctx : LCtx) (letDecl : LetDecl) : LCtx

def Lean.Compiler.LCNF.LCtx.addFunDecl (lctx : LCtx) (funDecl : FunDecl) : LCtx

def Lean.Compiler.LCNF.LCtx.eraseParam (lctx : LCtx) (param : Param) : LCtx

def Lean.Compiler.LCNF.LCtx.eraseParams (lctx : LCtx) (ps : Array Param) : LCtx

def Lean.Compiler.LCNF.LCtx.eraseLetDecl (lctx : LCtx) (decl : LetDecl) : LCtx

partial def Lean.Compiler.LCNF.LCtx.eraseFunDecl (lctx : LCtx) (decl : FunDecl) (recursive : Bool := true) : LCtx

partial def Lean.Compiler.LCNF.LCtx.eraseAlts (alts : Array Alt) (lctx : LCtx) : LCtx

partial def Lean.Compiler.LCNF.LCtx.eraseCode (code : Code) (lctx : LCtx) : LCtx

def Lean.Compiler.LCNF.LCtx.toLocalContext (lctx : LCtx) : LocalContext

Convert a LCNF local context into a regular Lean local context.