- letDecls : Lean.HashMap Lean.FVarId Lean.Compiler.LCNF.LetDecl
- funDecls : Lean.HashMap Lean.FVarId Lean.Compiler.LCNF.FunDecl
LCNF local context.
Instances For
def
Lean.Compiler.LCNF.LCtx.addParam
(lctx : Lean.Compiler.LCNF.LCtx)
(param : Lean.Compiler.LCNF.Param)
:
Instances For
def
Lean.Compiler.LCNF.LCtx.addLetDecl
(lctx : Lean.Compiler.LCNF.LCtx)
(letDecl : Lean.Compiler.LCNF.LetDecl)
:
Instances For
def
Lean.Compiler.LCNF.LCtx.addFunDecl
(lctx : Lean.Compiler.LCNF.LCtx)
(funDecl : Lean.Compiler.LCNF.FunDecl)
:
Instances For
def
Lean.Compiler.LCNF.LCtx.eraseParam
(lctx : Lean.Compiler.LCNF.LCtx)
(param : Lean.Compiler.LCNF.Param)
:
Instances For
def
Lean.Compiler.LCNF.LCtx.eraseParams
(lctx : Lean.Compiler.LCNF.LCtx)
(ps : Array Lean.Compiler.LCNF.Param)
:
Instances For
def
Lean.Compiler.LCNF.LCtx.eraseLetDecl
(lctx : Lean.Compiler.LCNF.LCtx)
(decl : Lean.Compiler.LCNF.LetDecl)
:
Instances For
partial def
Lean.Compiler.LCNF.LCtx.eraseFunDecl
(lctx : Lean.Compiler.LCNF.LCtx)
(decl : Lean.Compiler.LCNF.FunDecl)
(recursive : optParam Bool true)
:
partial def
Lean.Compiler.LCNF.LCtx.eraseAlts
(alts : Array Lean.Compiler.LCNF.Alt)
(lctx : Lean.Compiler.LCNF.LCtx)
:
partial def
Lean.Compiler.LCNF.LCtx.eraseCode
(code : Lean.Compiler.LCNF.Code)
(lctx : Lean.Compiler.LCNF.LCtx)
:
Convert a LCNF local context into a regular Lean local context.