LCNF local context.
- params : Std.HashMap FVarId Param
- letDecls : Std.HashMap FVarId LetDecl
- funDecls : Std.HashMap FVarId FunDecl
Instances For
Equations
- Lean.Compiler.LCNF.instInhabitedLCtx = { default := { params := default, letDecls := default, funDecls := default } }
Equations
- lctx.addLetDecl letDecl = { params := lctx.params, letDecls := lctx.letDecls.insert letDecl.fvarId letDecl, funDecls := lctx.funDecls }
Instances For
Equations
- lctx.addFunDecl funDecl = { params := lctx.params, letDecls := lctx.letDecls, funDecls := lctx.funDecls.insert funDecl.fvarId funDecl }
Instances For
Equations
- lctx.eraseParam param = { params := lctx.params.erase param.fvarId, letDecls := lctx.letDecls, funDecls := lctx.funDecls }
Instances For
Equations
- lctx.eraseLetDecl decl = { params := lctx.params, letDecls := lctx.letDecls.erase decl.fvarId, funDecls := lctx.funDecls }
Instances For
Convert a LCNF local context into a regular Lean local context.
Equations
- One or more equations did not get rendered due to their size.