structure Lean.Compiler.LCNF.LCtx : Type

LCNF local context.

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

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

Equations

• Lean.Compiler.LCNF.instInhabitedLCtx.default = { params := default, letDecls := default, funDecls := default }

instance Lean.Compiler.LCNF.instInhabitedLCtx : Inhabited LCtx

Equations

• Lean.Compiler.LCNF.instInhabitedLCtx = { default := Lean.Compiler.LCNF.instInhabitedLCtx.default }

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

Equations

• lctx.addParam param = { params := lctx.params.insert param.fvarId param, letDecls := lctx.letDecls, funDecls := lctx.funDecls }

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

Equations

• lctx.addLetDecl letDecl = { params := lctx.params, letDecls := lctx.letDecls.insert letDecl.fvarId letDecl, funDecls := lctx.funDecls }

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

Equations

• lctx.addFunDecl funDecl = { params := lctx.params, letDecls := lctx.letDecls, funDecls := lctx.funDecls.insert funDecl.fvarId funDecl }

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

Equations

• lctx.eraseParam param = { params := lctx.params.erase param.fvarId, letDecls := lctx.letDecls, funDecls := lctx.funDecls }

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

Equations

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

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

Equations

• lctx.eraseLetDecl decl = { params := lctx.params, letDecls := lctx.letDecls.erase decl.fvarId, funDecls := lctx.funDecls }

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.

Equations

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