structure Lean.Compiler.LCNF.LCtx : Type

• params : Lean.HashMap Lean.FVarId Lean.Compiler.LCNF.Param
• letDecls : Lean.HashMap Lean.FVarId Lean.Compiler.LCNF.LetDecl
• funDecls : Lean.HashMap Lean.FVarId Lean.Compiler.LCNF.FunDecl

LCNF local context.

instance Lean.Compiler.LCNF.instInhabitedLCtx : Inhabited Lean.Compiler.LCNF.LCtx

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

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

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

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

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

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

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

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

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

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

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