Skip to content

Commit 67f4543

Browse files
committed
chore: clean up structProjCases pass
1 parent 65a5d0c commit 67f4543

File tree

1 file changed

+4
-2
lines changed

1 file changed

+4
-2
lines changed

src/Lean/Compiler/LCNF/StructProjCases.lean

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff 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

4040
def M.run (x : M α) : CompilerM α := do
4141
x.run' {}
@@ -128,4 +128,6 @@ end StructProjCases
128128
def structProjCases : Pass :=
129129
.mkPerDeclaration `structProjCases (StructProjCases.visitDecl · |>.run) .mono
130130

131+
builtin_initialize registerTraceClass `Compiler.structProjCases (inherited := true)
132+
131133
end Lean.Compiler.LCNF

0 commit comments

Comments
 (0)