def Lean.Compiler.LCNF.StructProjCases.findStructCtorInfo? (typeName : Name) : CoreM (Option ConstructorVal)

def Lean.Compiler.LCNF.StructProjCases.mkFieldParamsForCtorType (e : Expr) (numParams : Nat) : CompilerM (Array Param)

def Lean.Compiler.LCNF.StructProjCases.mkFieldParamsForCtorType.loop (params : Array Param) (e : Expr) (numParams : Nat) : CompilerM (Array Param)

structure Lean.Compiler.LCNF.StructProjCases.State : Type

• projMap : Std.HashMap FVarId (Array FVarId)
• fvarMap : Std.HashMap FVarId FVarId

@[reducible, inline]

abbrev Lean.Compiler.LCNF.StructProjCases.M (α : Type) : Type

def Lean.Compiler.LCNF.StructProjCases.M.run {α : Type} (x : M α) : CompilerM α

def Lean.Compiler.LCNF.StructProjCases.remapFVar (fvarId : FVarId) : M FVarId

partial def Lean.Compiler.LCNF.StructProjCases.visitCode (code : Code) : M Code

def Lean.Compiler.LCNF.StructProjCases.visitLetValue (v : LetValue) : M LetValue

partial def Lean.Compiler.LCNF.StructProjCases.visitAlt (alt : Alt) : M Alt

def Lean.Compiler.LCNF.StructProjCases.visitArg (arg : Arg) : M Arg

def Lean.Compiler.LCNF.StructProjCases.visitDecl (decl : Decl) : M Decl

def Lean.Compiler.LCNF.structProjCases : Pass