structure Lean.Compiler.LCNF.LCtx : Type

LCNF local context.

• 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

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

Equations

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

def Lean.Compiler.LCNF.LCtx.addParam (lctx : Lean.Compiler.LCNF.LCtx) (param : Lean.Compiler.LCNF.Param) : Lean.Compiler.LCNF.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 : Lean.Compiler.LCNF.LCtx) (letDecl : Lean.Compiler.LCNF.LetDecl) : Lean.Compiler.LCNF.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 : Lean.Compiler.LCNF.LCtx) (funDecl : Lean.Compiler.LCNF.FunDecl) : Lean.Compiler.LCNF.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 : Lean.Compiler.LCNF.LCtx) (param : Lean.Compiler.LCNF.Param) : Lean.Compiler.LCNF.LCtx

Equations

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

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

Equations

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

def Lean.Compiler.LCNF.LCtx.eraseLetDecl (lctx : Lean.Compiler.LCNF.LCtx) (decl : Lean.Compiler.LCNF.LetDecl) : Lean.Compiler.LCNF.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 : 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.

Equations

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