Documentation

Lean.Compiler.LCNF.LCtx

Equations
Equations
  • lctx.addParam param = { params := lctx.params.insert param.fvarId param, letDecls := lctx.letDecls, funDecls := lctx.funDecls }
Equations
  • lctx.addLetDecl letDecl = { params := lctx.params, letDecls := lctx.letDecls.insert letDecl.fvarId letDecl, funDecls := lctx.funDecls }
Equations
  • lctx.addFunDecl funDecl = { params := lctx.params, letDecls := lctx.letDecls, funDecls := lctx.funDecls.insert funDecl.fvarId funDecl }
Equations
  • lctx.eraseParam param = { params := lctx.params.erase param.fvarId, letDecls := lctx.letDecls, funDecls := lctx.funDecls }
Equations
  • One or more equations did not get rendered due to their size.
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) :
partial def Lean.Compiler.LCNF.LCtx.eraseCode (code : Code) (lctx : LCtx) :

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

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