inductive Lean.IR.ToIR.FVarClassification : Type

• var (id : VarId) : FVarClassification
• joinPoint (id : JoinPointId) : FVarClassification
• erased : FVarClassification

structure Lean.IR.ToIR.BuilderState : Type

• fvars : Std.HashMap FVarId FVarClassification
• nextId : Nat

@[reducible, inline]

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

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

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

def Lean.IR.ToIR.bindVarToVarId (fvarId : FVarId) (varId : VarId) : M Unit

def Lean.IR.ToIR.newVar : M VarId

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

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

def Lean.IR.ToIR.findDecl (n : Name) : M (Option Decl)

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

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

def Lean.IR.ToIR.lowerEnumToScalarType (name : Name) : M (Option IRType)

def Lean.IR.ToIR.lowerType (e : Lean.Expr) : M IRType

def Lean.IR.ToIR.getCtorInfo (name : Name) : M (CtorInfo × Array CtorFieldInfo)

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

inductive Lean.IR.ToIR.TranslatedProj : Type

• expr (e : Expr) : TranslatedProj
• erased : TranslatedProj

instance Lean.IR.ToIR.instInhabitedTranslatedProj : Inhabited TranslatedProj

def Lean.IR.ToIR.lowerProj (base : VarId) (ctorInfo : CtorInfo) (field : CtorFieldInfo) : TranslatedProj × IRType

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

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

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

partial def Lean.IR.ToIR.lowerLet.mkVar (decl : Compiler.LCNF.LetDecl) (k : Compiler.LCNF.Code) (v : VarId) : M FnBody

partial def Lean.IR.ToIR.lowerLet.mkExpr (decl : Compiler.LCNF.LetDecl) (k : Compiler.LCNF.Code) (e : Expr) : M FnBody

partial def Lean.IR.ToIR.lowerLet.mkErased (decl : Compiler.LCNF.LetDecl) (k : Compiler.LCNF.Code) : Unit → M FnBody

partial def Lean.IR.ToIR.lowerLet.mkPartialApp (decl : Compiler.LCNF.LetDecl) (k : Compiler.LCNF.Code) (e : Expr) (restArgs : Array Arg) : M FnBody

partial def Lean.IR.ToIR.lowerLet.tryIrDecl? (decl : Compiler.LCNF.LetDecl) (k : Compiler.LCNF.Code) (name : Name) (args : Array Arg) : M (Option FnBody)

partial def Lean.IR.ToIR.lowerLet.lowerNonObjectFields (k : Compiler.LCNF.Code) (ctorInfo : CtorInfo) (fields : Array CtorFieldInfo) (args : Array Compiler.LCNF.Arg) (objVar : VarId) : Unit → M FnBody

partial def Lean.IR.ToIR.lowerLet.lowerNonObjectFields.loop (k : Compiler.LCNF.Code) (ctorInfo : CtorInfo) (fields : Array CtorFieldInfo) (args : Array Compiler.LCNF.Arg) (objVar : VarId) (usizeCount i : Nat) : M FnBody

partial def Lean.IR.ToIR.lowerAlt (discr : VarId) (a : Compiler.LCNF.Alt) : M Alt

partial def Lean.IR.ToIR.lowerAlt.loop (discr : VarId) (code : Compiler.LCNF.Code) (ctorInfo : CtorInfo) (params : Array Compiler.LCNF.Param) (fields : Array CtorFieldInfo) (i : Nat) : M FnBody

def Lean.IR.ToIR.lowerResultType (type : Lean.Expr) (arity : Nat) : M IRType

def Lean.IR.ToIR.lowerResultType.resultTypeForArity (type : Lean.Expr) (arity : Nat) : Lean.Expr

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

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