structure Lean.IR.ToIR.BuilderState : Type

• vars : Std.HashMap FVarId Arg
• joinPoints : Std.HashMap FVarId JoinPointId
• nextVarId : Nat
• nextJpId : Nat

@[reducible, inline]

abbrev Lean.IR.ToIR.M (α : Type) : Type

def Lean.IR.ToIR.M.run {α : Type} (x : M α) : CoreM α

def Lean.IR.ToIR.getFVarValue (fvarId : FVarId) : M Arg

def Lean.IR.ToIR.getJoinPointValue (fvarId : FVarId) : M JoinPointId

def Lean.IR.ToIR.bindVar (fvarId : FVarId) : M VarId

def Lean.IR.ToIR.bindJoinPoint (fvarId : FVarId) : M JoinPointId

def Lean.IR.ToIR.bindErased (fvarId : FVarId) : M Unit

def Lean.IR.ToIR.addDecl (d : Decl) : M Unit

def Lean.IR.ToIR.lowerLitValue (v : Compiler.LCNF.LitValue) : LitVal × IRType

def Lean.IR.ToIR.lowerArg (a : Compiler.LCNF.Arg Compiler.LCNF.Purity.impure) : M Arg

def Lean.IR.ToIR.lowerParam (p : Compiler.LCNF.Param Compiler.LCNF.Purity.impure) : M Param

@[inline]

def Lean.IR.ToIR.lowerCtorInfo (i : Compiler.LCNF.CtorInfo) : CtorInfo

partial def Lean.IR.ToIR.lowerCode (c : Compiler.LCNF.Code Compiler.LCNF.Purity.impure) : M FnBody

partial def Lean.IR.ToIR.lowerLet (decl : Compiler.LCNF.LetDecl Compiler.LCNF.Purity.impure) (k : Compiler.LCNF.Code Compiler.LCNF.Purity.impure) : M FnBody

partial def Lean.IR.ToIR.lowerAlt (a : Compiler.LCNF.Alt Compiler.LCNF.Purity.impure) : M Alt

def Lean.IR.ToIR.lowerDecl (d : Compiler.LCNF.Decl Compiler.LCNF.Purity.impure) : M (Option Decl)

def Lean.IR.toIR (decls : Array (Compiler.LCNF.Decl Compiler.LCNF.Purity.impure)) : CoreM (Array Decl)