structure Lean.Compiler.LCNF.LCtx : Type

LCNF local context.

• paramsPure : Std.HashMap FVarId (Param Purity.pure)
• paramsImpure : Std.HashMap FVarId (Param Purity.impure)
• letDeclsPure : Std.HashMap FVarId (LetDecl Purity.pure)
• letDeclsImpure : Std.HashMap FVarId (LetDecl Purity.impure)
• funDeclsPure : Std.HashMap FVarId (FunDecl Purity.pure)
• funDeclsImpure : Std.HashMap FVarId (FunDecl Purity.impure)

@[instance_reducible]

instance Lean.Compiler.LCNF.instInhabitedLCtx : Inhabited LCtx

Equations

• Lean.Compiler.LCNF.instInhabitedLCtx = { default := Lean.Compiler.LCNF.instInhabitedLCtx.default }

def Lean.Compiler.LCNF.instInhabitedLCtx.default : LCtx

Equations

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

def Lean.Compiler.LCNF.LCtx.addParam {pu : Purity} (lctx : LCtx) (param : Param pu) : LCtx

Equations

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

def Lean.Compiler.LCNF.LCtx.addLetDecl {pu : Purity} (lctx : LCtx) (letDecl : LetDecl pu) : LCtx

Equations

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

def Lean.Compiler.LCNF.LCtx.addFunDecl {pu : Purity} (lctx : LCtx) (funDecl : FunDecl pu) : LCtx

Equations

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

def Lean.Compiler.LCNF.LCtx.eraseParam {pu : Purity} (lctx : LCtx) (param : Param pu) : LCtx

Equations

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

def Lean.Compiler.LCNF.LCtx.eraseParams {pu : Purity} (lctx : LCtx) (ps : Array (Param pu)) : LCtx

Equations

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

def Lean.Compiler.LCNF.LCtx.eraseLetDecl {pu : Purity} (lctx : LCtx) (decl : LetDecl pu) : LCtx

Equations

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

partial def Lean.Compiler.LCNF.LCtx.eraseFunDecl {pu : Purity} (lctx : LCtx) (decl : FunDecl pu) (recursive : Bool := true) : LCtx

partial def Lean.Compiler.LCNF.LCtx.eraseAlts {pu : Purity} (alts : Array (Alt pu)) (lctx : LCtx) : LCtx

partial def Lean.Compiler.LCNF.LCtx.eraseCode {pu : Purity} (code : Code pu) (lctx : LCtx) : LCtx

@[inline]

def Lean.Compiler.LCNF.LCtx.params (lctx : LCtx) (pu : Purity) : Std.HashMap FVarId (Param pu)

Equations

• lctx.params Lean.Compiler.LCNF.Purity.pure = lctx.paramsPure
• lctx.params Lean.Compiler.LCNF.Purity.impure = lctx.paramsImpure

@[inline]

def Lean.Compiler.LCNF.LCtx.letDecls (lctx : LCtx) (pu : Purity) : Std.HashMap FVarId (LetDecl pu)

Equations

• lctx.letDecls Lean.Compiler.LCNF.Purity.pure = lctx.letDeclsPure
• lctx.letDecls Lean.Compiler.LCNF.Purity.impure = lctx.letDeclsImpure

@[inline]

def Lean.Compiler.LCNF.LCtx.funDecls (lctx : LCtx) (pu : Purity) : Std.HashMap FVarId (FunDecl pu)

Equations

• lctx.funDecls Lean.Compiler.LCNF.Purity.pure = lctx.funDeclsPure
• lctx.funDecls Lean.Compiler.LCNF.Purity.impure = lctx.funDeclsImpure

def Lean.Compiler.LCNF.LCtx.toLocalContext (lctx : LCtx) (pu : Purity) : 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.