structure Lean.Compiler.LCNF.LCtx : Type

LCNF local context.

• paramsPure : Std.HashMap FVarId (Param Purity.pure)
• paramsImpure : Std.HashMap FVarId (Param Purity.impure)
• letDeclsPure : Std.HashMap FVarId (LetDecl Purity.pure)
• letDeclsImpure : Std.HashMap FVarId (LetDecl Purity.impure)
• funDeclsPure : Std.HashMap FVarId (FunDecl Purity.pure)
• funDeclsImpure : Std.HashMap FVarId (FunDecl Purity.impure)

@[implicit_reducible]

instance Lean.Compiler.LCNF.instInhabitedLCtx : Inhabited LCtx

def Lean.Compiler.LCNF.instInhabitedLCtx.default : LCtx

def Lean.Compiler.LCNF.LCtx.addParam {pu : Purity} (lctx : LCtx) (param : Param pu) : LCtx

def Lean.Compiler.LCNF.LCtx.addLetDecl {pu : Purity} (lctx : LCtx) (letDecl : LetDecl pu) : LCtx

def Lean.Compiler.LCNF.LCtx.addFunDecl {pu : Purity} (lctx : LCtx) (funDecl : FunDecl pu) : LCtx

def Lean.Compiler.LCNF.LCtx.eraseParam {pu : Purity} (lctx : LCtx) (param : Param pu) : LCtx

def Lean.Compiler.LCNF.LCtx.eraseParams {pu : Purity} (lctx : LCtx) (ps : Array (Param pu)) : LCtx

def Lean.Compiler.LCNF.LCtx.eraseLetDecl {pu : Purity} (lctx : LCtx) (decl : LetDecl pu) : LCtx

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

partial def Lean.Compiler.LCNF.LCtx.eraseAlts {pu : Purity} (alts : Array (Alt pu)) (lctx : LCtx) : LCtx

partial def Lean.Compiler.LCNF.LCtx.eraseCode {pu : Purity} (code : Code pu) (lctx : LCtx) : LCtx

@[inline]

def Lean.Compiler.LCNF.LCtx.params (lctx : LCtx) (pu : Purity) : Std.HashMap FVarId (Param pu)

@[inline]

def Lean.Compiler.LCNF.LCtx.letDecls (lctx : LCtx) (pu : Purity) : Std.HashMap FVarId (LetDecl pu)

@[inline]

def Lean.Compiler.LCNF.LCtx.funDecls (lctx : LCtx) (pu : Purity) : Std.HashMap FVarId (FunDecl pu)

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

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