File tree Expand file tree Collapse file tree 1 file changed +4
-2
lines changed
Expand file tree Collapse file tree 1 file changed +4
-2
lines changed Original file line number Diff line number Diff line change @@ -31,11 +31,11 @@ def mkFieldParamsForCtorType (e : Expr) (numParams : Nat): CompilerM (Array Para
3131 | _ => return params
3232 loop #[] e numParams
3333
34- structure StructProjState where
34+ structure State where
3535 projMap : Std.HashMap FVarId (Array FVarId) := {}
3636 fvarMap : Std.HashMap FVarId FVarId := {}
3737
38- abbrev M := StateRefT StructProjState CompilerM
38+ abbrev M := StateRefT State CompilerM
3939
4040def M.run (x : M α) : CompilerM α := do
4141 x.run' {}
@@ -128,4 +128,6 @@ end StructProjCases
128128def structProjCases : Pass :=
129129 .mkPerDeclaration `structProjCases (StructProjCases.visitDecl · |>.run) .mono
130130
131+ builtin_initialize registerTraceClass `Compiler.structProjCases (inherited := true )
132+
131133end Lean.Compiler.LCNF
You can’t perform that action at this time.
0 commit comments