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

Equations

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

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

Equations

• Lean.Compiler.LCNF.StructProjCases.mkFieldParamsForCtorType e numParams = Lean.Compiler.LCNF.StructProjCases.mkFieldParamsForCtorType.loop #[] e numParams

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Compiler.LCNF.StructProjCases.mkFieldParamsForCtorType.loop params e numParams = pure params

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

Equations

• Lean.Compiler.LCNF.StructProjCases.M = StateRefT' IO.RealWorld Lean.Compiler.LCNF.StructProjCases.State Lean.Compiler.LCNF.CompilerM

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

Equations

• x.run = StateRefT'.run' x { }

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

Equations

• Lean.Compiler.LCNF.StructProjCases.remapFVar fvarId = do let __do_lift ← get pure (__do_lift.fvarMap[fvarId]?.getD fvarId)

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

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Compiler.LCNF.StructProjCases.visitLetValue (Lean.Compiler.LCNF.LetValue.lit value) = pure (Lean.Compiler.LCNF.LetValue.lit value)
• Lean.Compiler.LCNF.StructProjCases.visitLetValue Lean.Compiler.LCNF.LetValue.erased = pure Lean.Compiler.LCNF.LetValue.erased

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

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Compiler.LCNF.StructProjCases.visitArg (Lean.Compiler.LCNF.Arg.type expr) = pure (Lean.Compiler.LCNF.Arg.type expr)
• Lean.Compiler.LCNF.StructProjCases.visitArg Lean.Compiler.LCNF.Arg.erased = pure Lean.Compiler.LCNF.Arg.erased

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

Equations

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

def Lean.Compiler.LCNF.structProjCases : Pass

Equations

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