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 (ctorType : Expr) (numParams numFields : Nat) : CompilerM (Array (Param Purity.pure))

Equations

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

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 Purity.pure) : M (Code Purity.pure)

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

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 Purity.pure) : M (Alt Purity.pure)

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

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 Purity.pure) : M (Decl Purity.pure)

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.