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

• Lean.Compiler.LCNF.LCtx.addParam lctx param = { params := Lean.HashMap.insert lctx.params 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

• Lean.Compiler.LCNF.LCtx.addLetDecl lctx letDecl = { params := lctx.params, letDecls := Lean.HashMap.insert lctx.letDecls 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

• Lean.Compiler.LCNF.LCtx.addFunDecl lctx funDecl = { params := lctx.params, letDecls := lctx.letDecls, funDecls := Lean.HashMap.insert lctx.funDecls funDecl.fvarId funDecl }

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

Equations

• Lean.Compiler.LCNF.LCtx.eraseParam lctx param = { params := Lean.HashMap.erase lctx.params 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

• Lean.Compiler.LCNF.LCtx.eraseLetDecl lctx decl = { params := lctx.params, letDecls := Lean.HashMap.erase lctx.letDecls 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.