diff --git a/library/init/lean/compiler/elimdead.lean b/library/init/lean/compiler/elimdead.lean
index 36799982a8..3461bb48d9 100644
--- a/library/init/lean/compiler/elimdead.lean
+++ b/library/init/lean/compiler/elimdead.lean
@@ -41,7 +41,6 @@ partial def FnBody.elimDead : FnBody → FnBody
   reshapeWithoutDead bs term
 
 /-- Eliminate dead let-declarations and join points -/
-@[export lean.ir.decl_elim_dead_core]
 def Decl.elimDead : Decl → Decl
 | (Decl.fdecl f xs t b) := Decl.fdecl f xs t b.elimDead
 | other                 := other
diff --git a/library/init/lean/compiler/ir.lean b/library/init/lean/compiler/ir.lean
index d0f1f0d04d..0ee713c54b 100644
--- a/library/init/lean/compiler/ir.lean
+++ b/library/init/lean/compiler/ir.lean
@@ -655,11 +655,9 @@ partial def collectDecl : Decl → Collector
 
 end MaxVar
 
-@[export lean.ir.fnbody_max_var_core]
 def FnBody.maxVar (b : FnBody) : Index :=
 MaxVar.collectFnBody b 0
 
-@[export lean.ir.decl_max_var_core]
 def Decl.maxVar (d : Decl) : Index :=
 MaxVar.collectDecl d 0
 
diff --git a/library/init/lean/compiler/pushproj.lean b/library/init/lean/compiler/pushproj.lean
index aede9f72bc..f2a9e51398 100644
--- a/library/init/lean/compiler/pushproj.lean
+++ b/library/init/lean/compiler/pushproj.lean
@@ -47,7 +47,6 @@ partial def FnBody.pushProj : FnBody → FnBody
   | other := reshape bs term
 
 /-- Push projections inside `case` branches. -/
-@[export lean.ir.decl_push_proj_core]
 def Decl.pushProj : Decl → Decl
 | (Decl.fdecl f xs t b) := Decl.fdecl f xs t b.pushProj
 | other                 := other
diff --git a/library/init/lean/compiler/simpcase.lean b/library/init/lean/compiler/simpcase.lean
index 08c85d1ff9..f431073a23 100644
--- a/library/init/lean/compiler/simpcase.lean
+++ b/library/init/lean/compiler/simpcase.lean
@@ -48,7 +48,6 @@ partial def FnBody.simpCase : FnBody → FnBody
   - Remove unreachable branches.
   - Remove `case` if there is only one branch.
   - Merge most common branches using `Alt.default`. -/
-@[export lean.ir.decl_simp_case_core]
 def Decl.simpCase : Decl → Decl
 | (Decl.fdecl f xs t b) := Decl.fdecl f xs t b.simpCase
 | other                 := other
diff --git a/src/stage0/init/lean/compiler/default.cpp b/src/stage0/init/lean/compiler/default.cpp
index 7c3ab8f8fc..af3b9de933 100644
--- a/src/stage0/init/lean/compiler/default.cpp
+++ b/src/stage0/init/lean/compiler/default.cpp
@@ -26,8 +26,14 @@ obj* decl_to_string_core(obj*);
 extern "C" obj* lean_io_prim_put_str(obj*, obj*);
 obj* l_IO_println___at_Lean_IR_test___spec__1(obj*, obj*);
 obj* l_Lean_IR_Decl_pushProj___main(obj*);
+obj* l_Nat_repr(obj*);
+obj* l_Lean_IR_MaxVar_collectDecl___main(obj*, obj*);
+namespace lean {
+obj* string_append(obj*, obj*);
+}
 obj* l_Lean_IR_test___closed__1;
 obj* l_Lean_IR_Decl_elimDead___main(obj*);
+obj* l_Lean_IR_test___closed__4;
 obj* l_IO_println___at_HasRepr_HasEval___spec__1(obj*, obj*);
 obj* l_IO_print___at_Lean_IR_test___spec__2(obj*, obj*);
 obj* l_Lean_IR_Decl_simpCase___main(obj*);
@@ -100,7 +106,7 @@ obj* _init_l_Lean_IR_test___closed__1() {
 _start:
 {
 obj* x_0; 
-x_0 = lean::mk_string("=== After push projections ===");
+x_0 = lean::mk_string("Max variable ");
 return x_0;
 }
 }
@@ -108,7 +114,7 @@ obj* _init_l_Lean_IR_test___closed__2() {
 _start:
 {
 obj* x_0; 
-x_0 = lean::mk_string("=== After elim dead locals ===");
+x_0 = lean::mk_string("=== After push projections ===");
 return x_0;
 }
 }
@@ -116,6 +122,14 @@ obj* _init_l_Lean_IR_test___closed__3() {
 _start:
 {
 obj* x_0; 
+x_0 = lean::mk_string("=== After elim dead locals ===");
+return x_0;
+}
+}
+obj* _init_l_Lean_IR_test___closed__4() {
+_start:
+{
+obj* x_0; 
 x_0 = lean::mk_string("=== After simplify case ===");
 return x_0;
 }
@@ -130,7 +144,7 @@ lean::inc(x_0);
 x_3 = l_IO_println___at_Lean_IR_test___spec__1(x_0, x_1);
 if (lean::obj_tag(x_3) == 0)
 {
-obj* x_4; obj* x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_10; obj* x_11; 
+obj* x_4; obj* x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_11; obj* x_12; obj* x_13; obj* x_14; obj* x_16; 
 x_4 = lean::cnstr_get(x_3, 1);
 if (lean::is_exclusive(x_3)) {
  lean::cnstr_release(x_3, 0);
@@ -148,40 +162,25 @@ if (lean::is_scalar(x_6)) {
 }
 lean::cnstr_set(x_8, 0, x_7);
 lean::cnstr_set(x_8, 1, x_4);
-x_9 = l_Lean_IR_Decl_pushProj___main(x_0);
-x_10 = l_Lean_IR_test___closed__1;
-x_11 = l_IO_println___at_HasRepr_HasEval___spec__1(x_10, x_8);
-if (lean::obj_tag(x_11) == 0)
-{
-obj* x_12; obj* x_14; obj* x_15; obj* x_17; 
-x_12 = lean::cnstr_get(x_11, 1);
-if (lean::is_exclusive(x_11)) {
- lean::cnstr_release(x_11, 0);
- x_14 = x_11;
-} else {
- lean::inc(x_12);
- lean::dec(x_11);
- x_14 = lean::box(0);
-}
-if (lean::is_scalar(x_14)) {
- x_15 = lean::alloc_cnstr(0, 2, 0);
-} else {
- x_15 = x_14;
-}
-lean::cnstr_set(x_15, 0, x_7);
-lean::cnstr_set(x_15, 1, x_12);
-lean::inc(x_9);
-x_17 = l_IO_println___at_Lean_IR_test___spec__1(x_9, x_15);
-if (lean::obj_tag(x_17) == 0)
+x_9 = lean::mk_nat_obj(0ul);
+lean::inc(x_0);
+x_11 = l_Lean_IR_MaxVar_collectDecl___main(x_0, x_9);
+x_12 = l_Nat_repr(x_11);
+x_13 = l_Lean_IR_test___closed__1;
+x_14 = lean::string_append(x_13, x_12);
+lean::dec(x_12);
+x_16 = l_IO_println___at_HasRepr_HasEval___spec__1(x_14, x_8);
+lean::dec(x_14);
+if (lean::obj_tag(x_16) == 0)
 {
 obj* x_18; obj* x_20; obj* x_21; obj* x_22; obj* x_23; obj* x_24; 
-x_18 = lean::cnstr_get(x_17, 1);
-if (lean::is_exclusive(x_17)) {
- lean::cnstr_release(x_17, 0);
- x_20 = x_17;
+x_18 = lean::cnstr_get(x_16, 1);
+if (lean::is_exclusive(x_16)) {
+ lean::cnstr_release(x_16, 0);
+ x_20 = x_16;
 } else {
  lean::inc(x_18);
- lean::dec(x_17);
+ lean::dec(x_16);
  x_20 = lean::box(0);
 }
 if (lean::is_scalar(x_20)) {
@@ -191,7 +190,7 @@ if (lean::is_scalar(x_20)) {
 }
 lean::cnstr_set(x_21, 0, x_7);
 lean::cnstr_set(x_21, 1, x_18);
-x_22 = l_Lean_IR_Decl_elimDead___main(x_9);
+x_22 = l_Lean_IR_Decl_pushProj___main(x_0);
 x_23 = l_Lean_IR_test___closed__2;
 x_24 = l_IO_println___at_HasRepr_HasEval___spec__1(x_23, x_21);
 if (lean::obj_tag(x_24) == 0)
@@ -234,12 +233,12 @@ if (lean::is_scalar(x_33)) {
 }
 lean::cnstr_set(x_34, 0, x_7);
 lean::cnstr_set(x_34, 1, x_31);
-x_35 = l_Lean_IR_Decl_simpCase___main(x_22);
+x_35 = l_Lean_IR_Decl_elimDead___main(x_22);
 x_36 = l_Lean_IR_test___closed__3;
 x_37 = l_IO_println___at_HasRepr_HasEval___spec__1(x_36, x_34);
 if (lean::obj_tag(x_37) == 0)
 {
-obj* x_38; obj* x_40; obj* x_41; obj* x_42; 
+obj* x_38; obj* x_40; obj* x_41; obj* x_43; 
 x_38 = lean::cnstr_get(x_37, 1);
 if (lean::is_exclusive(x_37)) {
  lean::cnstr_release(x_37, 0);
@@ -256,151 +255,218 @@ if (lean::is_scalar(x_40)) {
 }
 lean::cnstr_set(x_41, 0, x_7);
 lean::cnstr_set(x_41, 1, x_38);
-x_42 = l_IO_println___at_Lean_IR_test___spec__1(x_35, x_41);
-return x_42;
-}
-else
+lean::inc(x_35);
+x_43 = l_IO_println___at_Lean_IR_test___spec__1(x_35, x_41);
+if (lean::obj_tag(x_43) == 0)
 {
-obj* x_44; obj* x_46; obj* x_48; obj* x_49; 
-lean::dec(x_35);
-x_44 = lean::cnstr_get(x_37, 0);
-x_46 = lean::cnstr_get(x_37, 1);
-if (lean::is_exclusive(x_37)) {
- x_48 = x_37;
+obj* x_44; obj* x_46; obj* x_47; obj* x_48; obj* x_49; obj* x_50; 
+x_44 = lean::cnstr_get(x_43, 1);
+if (lean::is_exclusive(x_43)) {
+ lean::cnstr_release(x_43, 0);
+ x_46 = x_43;
 } else {
  lean::inc(x_44);
- lean::inc(x_46);
- lean::dec(x_37);
- x_48 = lean::box(0);
+ lean::dec(x_43);
+ x_46 = lean::box(0);
 }
-if (lean::is_scalar(x_48)) {
- x_49 = lean::alloc_cnstr(1, 2, 0);
+if (lean::is_scalar(x_46)) {
+ x_47 = lean::alloc_cnstr(0, 2, 0);
 } else {
- x_49 = x_48;
+ x_47 = x_46;
 }
-lean::cnstr_set(x_49, 0, x_44);
-lean::cnstr_set(x_49, 1, x_46);
-return x_49;
-}
-}
-else
+lean::cnstr_set(x_47, 0, x_7);
+lean::cnstr_set(x_47, 1, x_44);
+x_48 = l_Lean_IR_Decl_simpCase___main(x_35);
+x_49 = l_Lean_IR_test___closed__4;
+x_50 = l_IO_println___at_HasRepr_HasEval___spec__1(x_49, x_47);
+if (lean::obj_tag(x_50) == 0)
 {
-obj* x_51; obj* x_53; obj* x_55; obj* x_56; 
-lean::dec(x_22);
-x_51 = lean::cnstr_get(x_30, 0);
-x_53 = lean::cnstr_get(x_30, 1);
-if (lean::is_exclusive(x_30)) {
- x_55 = x_30;
+obj* x_51; obj* x_53; obj* x_54; obj* x_55; 
+x_51 = lean::cnstr_get(x_50, 1);
+if (lean::is_exclusive(x_50)) {
+ lean::cnstr_release(x_50, 0);
+ x_53 = x_50;
 } else {
  lean::inc(x_51);
- lean::inc(x_53);
- lean::dec(x_30);
- x_55 = lean::box(0);
+ lean::dec(x_50);
+ x_53 = lean::box(0);
 }
-if (lean::is_scalar(x_55)) {
- x_56 = lean::alloc_cnstr(1, 2, 0);
+if (lean::is_scalar(x_53)) {
+ x_54 = lean::alloc_cnstr(0, 2, 0);
 } else {
- x_56 = x_55;
+ x_54 = x_53;
 }
-lean::cnstr_set(x_56, 0, x_51);
-lean::cnstr_set(x_56, 1, x_53);
-return x_56;
+lean::cnstr_set(x_54, 0, x_7);
+lean::cnstr_set(x_54, 1, x_51);
+x_55 = l_IO_println___at_Lean_IR_test___spec__1(x_48, x_54);
+return x_55;
+}
+else
+{
+obj* x_57; obj* x_59; obj* x_61; obj* x_62; 
+lean::dec(x_48);
+x_57 = lean::cnstr_get(x_50, 0);
+x_59 = lean::cnstr_get(x_50, 1);
+if (lean::is_exclusive(x_50)) {
+ x_61 = x_50;
+} else {
+ lean::inc(x_57);
+ lean::inc(x_59);
+ lean::dec(x_50);
+ x_61 = lean::box(0);
+}
+if (lean::is_scalar(x_61)) {
+ x_62 = lean::alloc_cnstr(1, 2, 0);
+} else {
+ x_62 = x_61;
+}
+lean::cnstr_set(x_62, 0, x_57);
+lean::cnstr_set(x_62, 1, x_59);
+return x_62;
 }
 }
 else
 {
-obj* x_58; obj* x_60; obj* x_62; obj* x_63; 
+obj* x_64; obj* x_66; obj* x_68; obj* x_69; 
+lean::dec(x_35);
+x_64 = lean::cnstr_get(x_43, 0);
+x_66 = lean::cnstr_get(x_43, 1);
+if (lean::is_exclusive(x_43)) {
+ x_68 = x_43;
+} else {
+ lean::inc(x_64);
+ lean::inc(x_66);
+ lean::dec(x_43);
+ x_68 = lean::box(0);
+}
+if (lean::is_scalar(x_68)) {
+ x_69 = lean::alloc_cnstr(1, 2, 0);
+} else {
+ x_69 = x_68;
+}
+lean::cnstr_set(x_69, 0, x_64);
+lean::cnstr_set(x_69, 1, x_66);
+return x_69;
+}
+}
+else
+{
+obj* x_71; obj* x_73; obj* x_75; obj* x_76; 
+lean::dec(x_35);
+x_71 = lean::cnstr_get(x_37, 0);
+x_73 = lean::cnstr_get(x_37, 1);
+if (lean::is_exclusive(x_37)) {
+ x_75 = x_37;
+} else {
+ lean::inc(x_71);
+ lean::inc(x_73);
+ lean::dec(x_37);
+ x_75 = lean::box(0);
+}
+if (lean::is_scalar(x_75)) {
+ x_76 = lean::alloc_cnstr(1, 2, 0);
+} else {
+ x_76 = x_75;
+}
+lean::cnstr_set(x_76, 0, x_71);
+lean::cnstr_set(x_76, 1, x_73);
+return x_76;
+}
+}
+else
+{
+obj* x_78; obj* x_80; obj* x_82; obj* x_83; 
 lean::dec(x_22);
-x_58 = lean::cnstr_get(x_24, 0);
-x_60 = lean::cnstr_get(x_24, 1);
+x_78 = lean::cnstr_get(x_30, 0);
+x_80 = lean::cnstr_get(x_30, 1);
+if (lean::is_exclusive(x_30)) {
+ x_82 = x_30;
+} else {
+ lean::inc(x_78);
+ lean::inc(x_80);
+ lean::dec(x_30);
+ x_82 = lean::box(0);
+}
+if (lean::is_scalar(x_82)) {
+ x_83 = lean::alloc_cnstr(1, 2, 0);
+} else {
+ x_83 = x_82;
+}
+lean::cnstr_set(x_83, 0, x_78);
+lean::cnstr_set(x_83, 1, x_80);
+return x_83;
+}
+}
+else
+{
+obj* x_85; obj* x_87; obj* x_89; obj* x_90; 
+lean::dec(x_22);
+x_85 = lean::cnstr_get(x_24, 0);
+x_87 = lean::cnstr_get(x_24, 1);
 if (lean::is_exclusive(x_24)) {
- x_62 = x_24;
+ x_89 = x_24;
 } else {
- lean::inc(x_58);
- lean::inc(x_60);
+ lean::inc(x_85);
+ lean::inc(x_87);
  lean::dec(x_24);
- x_62 = lean::box(0);
+ x_89 = lean::box(0);
 }
-if (lean::is_scalar(x_62)) {
- x_63 = lean::alloc_cnstr(1, 2, 0);
+if (lean::is_scalar(x_89)) {
+ x_90 = lean::alloc_cnstr(1, 2, 0);
 } else {
- x_63 = x_62;
+ x_90 = x_89;
 }
-lean::cnstr_set(x_63, 0, x_58);
-lean::cnstr_set(x_63, 1, x_60);
-return x_63;
+lean::cnstr_set(x_90, 0, x_85);
+lean::cnstr_set(x_90, 1, x_87);
+return x_90;
 }
 }
 else
 {
-obj* x_65; obj* x_67; obj* x_69; obj* x_70; 
-lean::dec(x_9);
-x_65 = lean::cnstr_get(x_17, 0);
-x_67 = lean::cnstr_get(x_17, 1);
-if (lean::is_exclusive(x_17)) {
- x_69 = x_17;
-} else {
- lean::inc(x_65);
- lean::inc(x_67);
- lean::dec(x_17);
- x_69 = lean::box(0);
-}
-if (lean::is_scalar(x_69)) {
- x_70 = lean::alloc_cnstr(1, 2, 0);
-} else {
- x_70 = x_69;
-}
-lean::cnstr_set(x_70, 0, x_65);
-lean::cnstr_set(x_70, 1, x_67);
-return x_70;
-}
-}
-else
-{
-obj* x_72; obj* x_74; obj* x_76; obj* x_77; 
-lean::dec(x_9);
-x_72 = lean::cnstr_get(x_11, 0);
-x_74 = lean::cnstr_get(x_11, 1);
-if (lean::is_exclusive(x_11)) {
- x_76 = x_11;
-} else {
- lean::inc(x_72);
- lean::inc(x_74);
- lean::dec(x_11);
- x_76 = lean::box(0);
-}
-if (lean::is_scalar(x_76)) {
- x_77 = lean::alloc_cnstr(1, 2, 0);
-} else {
- x_77 = x_76;
-}
-lean::cnstr_set(x_77, 0, x_72);
-lean::cnstr_set(x_77, 1, x_74);
-return x_77;
-}
-}
-else
-{
-obj* x_79; obj* x_81; obj* x_83; obj* x_84; 
+obj* x_92; obj* x_94; obj* x_96; obj* x_97; 
 lean::dec(x_0);
-x_79 = lean::cnstr_get(x_3, 0);
-x_81 = lean::cnstr_get(x_3, 1);
+x_92 = lean::cnstr_get(x_16, 0);
+x_94 = lean::cnstr_get(x_16, 1);
+if (lean::is_exclusive(x_16)) {
+ x_96 = x_16;
+} else {
+ lean::inc(x_92);
+ lean::inc(x_94);
+ lean::dec(x_16);
+ x_96 = lean::box(0);
+}
+if (lean::is_scalar(x_96)) {
+ x_97 = lean::alloc_cnstr(1, 2, 0);
+} else {
+ x_97 = x_96;
+}
+lean::cnstr_set(x_97, 0, x_92);
+lean::cnstr_set(x_97, 1, x_94);
+return x_97;
+}
+}
+else
+{
+obj* x_99; obj* x_101; obj* x_103; obj* x_104; 
+lean::dec(x_0);
+x_99 = lean::cnstr_get(x_3, 0);
+x_101 = lean::cnstr_get(x_3, 1);
 if (lean::is_exclusive(x_3)) {
- x_83 = x_3;
+ x_103 = x_3;
 } else {
- lean::inc(x_79);
- lean::inc(x_81);
+ lean::inc(x_99);
+ lean::inc(x_101);
  lean::dec(x_3);
- x_83 = lean::box(0);
+ x_103 = lean::box(0);
 }
-if (lean::is_scalar(x_83)) {
- x_84 = lean::alloc_cnstr(1, 2, 0);
+if (lean::is_scalar(x_103)) {
+ x_104 = lean::alloc_cnstr(1, 2, 0);
 } else {
- x_84 = x_83;
+ x_104 = x_103;
 }
-lean::cnstr_set(x_84, 0, x_79);
-lean::cnstr_set(x_84, 1, x_81);
-return x_84;
+lean::cnstr_set(x_104, 0, x_99);
+lean::cnstr_set(x_104, 1, x_101);
+return x_104;
 }
 }
 }
@@ -431,5 +497,7 @@ lean::mark_persistent(l_Lean_IR_test___closed__1);
 lean::mark_persistent(l_Lean_IR_test___closed__2);
  l_Lean_IR_test___closed__3 = _init_l_Lean_IR_test___closed__3();
 lean::mark_persistent(l_Lean_IR_test___closed__3);
+ l_Lean_IR_test___closed__4 = _init_l_Lean_IR_test___closed__4();
+lean::mark_persistent(l_Lean_IR_test___closed__4);
 return w;
 }
diff --git a/src/stage0/init/lean/compiler/elimdead.cpp b/src/stage0/init/lean/compiler/elimdead.cpp
index 5612b66d20..9467876be2 100644
--- a/src/stage0/init/lean/compiler/elimdead.cpp
+++ b/src/stage0/init/lean/compiler/elimdead.cpp
@@ -30,10 +30,7 @@ obj* l_Lean_IR_reshapeWithoutDeadAux___main(obj*, obj*, obj*);
 namespace lean {
 uint8 nat_dec_lt(obj*, obj*);
 }
-namespace lean {
-namespace ir {
-obj* decl_elim_dead_core(obj*);
-}}
+obj* l_Lean_IR_Decl_elimDead(obj*);
 obj* l_RBNode_findCore___main___at___private_init_lean_compiler_ir_2__collectIndex___spec__1(obj*, obj*);
 obj* l_Lean_IR_FnBody_flatten(obj*);
 namespace lean {
@@ -431,9 +428,7 @@ return x_0;
 }
 }
 }
-namespace lean {
-namespace ir {
-obj* decl_elim_dead_core(obj* x_0) {
+obj* l_Lean_IR_Decl_elimDead(obj* x_0) {
 _start:
 {
 obj* x_1; 
@@ -441,7 +436,6 @@ x_1 = l_Lean_IR_Decl_elimDead___main(x_0);
 return x_1;
 }
 }
-}}
 obj* initialize_init_default(obj*);
 obj* initialize_init_lean_compiler_ir(obj*);
 static bool _G_initialized = false;
diff --git a/src/stage0/init/lean/compiler/ir.cpp b/src/stage0/init/lean/compiler/ir.cpp
index 7bb1b0c5f1..5ed9d466b7 100644
--- a/src/stage0/init/lean/compiler/ir.cpp
+++ b/src/stage0/init/lean/compiler/ir.cpp
@@ -150,10 +150,7 @@ obj* l_Lean_IR_declHasFormat;
 obj* l___private_init_lean_compiler_ir_20__formatIRType___boxed(obj*);
 obj* l___private_init_lean_compiler_ir_19__formatExpr___main___closed__2;
 obj* l_Lean_IR_Alt_default(obj*);
-namespace lean {
-namespace ir {
-obj* decl_max_var_core(obj*);
-}}
+obj* l_Lean_IR_Decl_maxVar(obj*);
 obj* l___private_init_lean_compiler_ir_2__collectIndex(obj*, obj*, obj*);
 namespace lean {
 namespace ir {
@@ -354,10 +351,7 @@ obj* l___private_init_lean_compiler_ir_8__withParams___boxed(obj*, obj*, obj*, o
 obj* l_Lean_IR_VarId_lt___boxed(obj*, obj*);
 obj* l_Lean_IR_mkDecl___boxed(obj*, obj*, obj*, obj*);
 obj* l_Lean_IR_formatFnBody___main___closed__16;
-namespace lean {
-namespace ir {
-obj* fnbody_max_var_core(obj*);
-}}
+obj* l_Lean_IR_FnBody_maxVar(obj*);
 uint8 l_Lean_IR_CtorInfo_beq___main(obj*, obj*);
 uint8 l_Lean_IR_FnBody_beq(obj*, obj*);
 obj* l___private_init_lean_compiler_ir_14__collectAlts___boxed(obj*, obj*, obj*, obj*);
@@ -400,6 +394,7 @@ obj* l_Lean_IR_FnBody_isPure___main___boxed(obj*);
 obj* l_Lean_IR_litValHasFormat;
 uint8 l_Lean_IR_Alt_isDefault(obj*);
 obj* l_Array_miterateAux___main___at___private_init_lean_compiler_ir_16__formatArray___spec__1___boxed(obj*);
+obj* l_Lean_IR_fnBodyHasToString(obj*);
 obj* l_Lean_IR_FnBody_body___main(obj*);
 extern obj* l_Lean_Name_toString___closed__1;
 obj* l_Lean_IR_MaxVar_collectFnBody___main(obj*, obj*);
@@ -10921,6 +10916,17 @@ lean::closure_set(x_1, 0, x_0);
 return x_1;
 }
 }
+obj* l_Lean_IR_fnBodyHasToString(obj* x_0) {
+_start:
+{
+obj* x_1; obj* x_2; obj* x_3; obj* x_4; 
+x_1 = lean::mk_nat_obj(2ul);
+x_2 = l_Lean_IR_formatFnBody___main(x_1, x_0);
+x_3 = l_Lean_Options_empty;
+x_4 = l_Lean_Format_pretty(x_2, x_3);
+return x_4;
+}
+}
 obj* _init_l_Lean_IR_formatDecl___main___closed__1() {
 _start:
 {
@@ -12138,9 +12144,7 @@ x_2 = l_Lean_IR_MaxVar_collectDecl___main(x_0, x_1);
 return x_2;
 }
 }
-namespace lean {
-namespace ir {
-obj* fnbody_max_var_core(obj* x_0) {
+obj* l_Lean_IR_FnBody_maxVar(obj* x_0) {
 _start:
 {
 obj* x_1; obj* x_2; 
@@ -12149,10 +12153,7 @@ x_2 = l_Lean_IR_MaxVar_collectFnBody___main(x_0, x_1);
 return x_2;
 }
 }
-}}
-namespace lean {
-namespace ir {
-obj* decl_max_var_core(obj* x_0) {
+obj* l_Lean_IR_Decl_maxVar(obj* x_0) {
 _start:
 {
 obj* x_1; obj* x_2; 
@@ -12161,7 +12162,6 @@ x_2 = l_Lean_IR_MaxVar_collectDecl___main(x_0, x_1);
 return x_2;
 }
 }
-}}
 obj* initialize_init_lean_name(obj*);
 obj* initialize_init_lean_kvmap(obj*);
 obj* initialize_init_lean_format(obj*);
diff --git a/src/stage0/init/lean/compiler/pushproj.cpp b/src/stage0/init/lean/compiler/pushproj.cpp
index 122ce8d78d..23e727de42 100644
--- a/src/stage0/init/lean/compiler/pushproj.cpp
+++ b/src/stage0/init/lean/compiler/pushproj.cpp
@@ -22,10 +22,7 @@ namespace lean {
 obj* nat_sub(obj*, obj*);
 }
 extern obj* l_Lean_IR_vsetInh;
-namespace lean {
-namespace ir {
-obj* decl_push_proj_core(obj*);
-}}
+obj* l_Lean_IR_Decl_pushProj(obj*);
 obj* l_RBNode_ins___main___at___private_init_lean_compiler_ir_2__collectIndex___spec__2(obj*, obj*, obj*);
 obj* l_Lean_IR_pushProjs___main___closed__1;
 obj* l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__4___boxed(obj*, obj*, obj*, obj*, obj*);
@@ -829,9 +826,7 @@ return x_0;
 }
 }
 }
-namespace lean {
-namespace ir {
-obj* decl_push_proj_core(obj* x_0) {
+obj* l_Lean_IR_Decl_pushProj(obj* x_0) {
 _start:
 {
 obj* x_1; 
@@ -839,7 +834,6 @@ x_1 = l_Lean_IR_Decl_pushProj___main(x_0);
 return x_1;
 }
 }
-}}
 obj* initialize_init_default(obj*);
 obj* initialize_init_lean_compiler_ir(obj*);
 static bool _G_initialized = false;
diff --git a/src/stage0/init/lean/compiler/simpcase.cpp b/src/stage0/init/lean/compiler/simpcase.cpp
index e84abf4061..ee55dc856d 100644
--- a/src/stage0/init/lean/compiler/simpcase.cpp
+++ b/src/stage0/init/lean/compiler/simpcase.cpp
@@ -15,11 +15,11 @@ typedef lean::uint32 uint32; typedef lean::uint64 uint64;
 #pragma GCC diagnostic ignored "-Wunused-but-set-variable"
 #endif
 obj* l_Array_miterateAux___main___at___private_init_lean_compiler_simpcase_1__maxOccs___spec__2___boxed(obj*, obj*, obj*, obj*);
-obj* l_Array_filterAux___main___at___private_init_lean_compiler_simpcase_3__mkCase___spec__1(obj*, obj*, obj*);
 obj* l_Lean_IR_FnBody_simpCase(obj*);
 obj* l_Lean_IR_FnBody_simpCase___main(obj*);
 obj* l_Array_anyAux___main___at___private_init_lean_compiler_simpcase_2__addDefault___spec__1___boxed(obj*, obj*);
 obj* l_Array_miterateAux___main___at___private_init_lean_compiler_simpcase_1__maxOccs___spec__1___boxed(obj*, obj*, obj*, obj*, obj*);
+obj* l_Array_hmmapAux___main___at_Lean_IR_FnBody_simpCase___main___spec__2___closed__1;
 obj* l_Array_filterAux___main___at___private_init_lean_compiler_simpcase_2__addDefault___spec__2___boxed(obj*, obj*, obj*, obj*);
 obj* l_Lean_IR_reshape(obj*, obj*);
 obj* l_Array_filterAux___main___at___private_init_lean_compiler_simpcase_2__addDefault___spec__2(obj*, obj*, obj*, obj*);
@@ -27,7 +27,6 @@ namespace lean {
 uint8 nat_dec_lt(obj*, obj*);
 }
 obj* l_Array_miterateAux___main___at___private_init_lean_compiler_simpcase_1__maxOccs___spec__2(obj*, obj*, obj*, obj*);
-obj* l___private_init_lean_compiler_simpcase_3__mkCase(obj*, obj*, obj*);
 obj* l_Lean_IR_FnBody_flatten(obj*);
 obj* l___private_init_lean_compiler_simpcase_2__addDefault(obj*);
 namespace lean {
@@ -37,13 +36,13 @@ namespace lean {
 uint8 nat_dec_eq(obj*, obj*);
 }
 obj* l___private_init_lean_compiler_simpcase_1__maxOccs___boxed(obj*);
+obj* l_Array_filterAux___main___at___private_init_lean_compiler_simpcase_3__mkSimpCase___spec__1(obj*, obj*, obj*);
 extern obj* l_Lean_IR_altInh;
 uint8 l_Lean_IR_Alt_isDefault___main(obj*);
 uint8 l_Array_anyAux___main___at___private_init_lean_compiler_simpcase_2__addDefault___spec__1(obj*, obj*);
-namespace lean {
-namespace ir {
-obj* decl_simp_case_core(obj*);
-}}
+obj* l_Lean_IR_Decl_simpCase(obj*);
+obj* l___private_init_lean_compiler_simpcase_3__mkSimpCase(obj*, obj*, obj*);
+obj* l_Array_hmmapAux___main___at_Lean_IR_FnBody_simpCase___main___spec__2(obj*, obj*);
 obj* l_Array_shrink___main___rarg(obj*, obj*);
 obj* l_Lean_IR_AltCore_body___main(obj*);
 uint8 l_Lean_IR_FnBody_beq(obj*, obj*);
@@ -253,47 +252,47 @@ x_13 = l_Lean_IR_AltCore_body___main(x_0);
 x_14 = l_Lean_IR_FnBody_beq(x_11, x_13);
 if (x_14 == 0)
 {
-obj* x_15; obj* x_16; 
-x_15 = lean::mk_nat_obj(1ul);
-x_16 = lean::nat_add(x_2, x_15);
+uint8 x_15; 
+x_15 = lean::nat_dec_lt(x_3, x_2);
+if (x_15 == 0)
+{
+obj* x_16; obj* x_17; obj* x_19; 
+x_16 = lean::mk_nat_obj(1ul);
+x_17 = lean::nat_add(x_2, x_16);
 lean::dec(x_2);
-x_2 = x_16;
+x_19 = lean::nat_add(x_3, x_16);
+lean::dec(x_3);
+x_2 = x_17;
+x_3 = x_19;
 goto _start;
 }
 else
 {
-uint8 x_19; 
-x_19 = lean::nat_dec_lt(x_3, x_2);
-if (x_19 == 0)
-{
-obj* x_20; obj* x_21; obj* x_23; 
-x_20 = lean::mk_nat_obj(1ul);
-x_21 = lean::nat_add(x_2, x_20);
+obj* x_22; obj* x_23; obj* x_24; obj* x_26; 
+x_22 = lean::array_fswap(x_1, x_2, x_3);
+x_23 = lean::mk_nat_obj(1ul);
+x_24 = lean::nat_add(x_2, x_23);
 lean::dec(x_2);
-x_23 = lean::nat_add(x_3, x_20);
+x_26 = lean::nat_add(x_3, x_23);
 lean::dec(x_3);
-x_2 = x_21;
-x_3 = x_23;
+x_1 = x_22;
+x_2 = x_24;
+x_3 = x_26;
 goto _start;
 }
+}
 else
 {
-obj* x_26; obj* x_27; obj* x_28; obj* x_30; 
-x_26 = lean::array_fswap(x_1, x_2, x_3);
-x_27 = lean::mk_nat_obj(1ul);
-x_28 = lean::nat_add(x_2, x_27);
+obj* x_29; obj* x_30; 
+x_29 = lean::mk_nat_obj(1ul);
+x_30 = lean::nat_add(x_2, x_29);
 lean::dec(x_2);
-x_30 = lean::nat_add(x_3, x_27);
-lean::dec(x_3);
-x_1 = x_26;
-x_2 = x_28;
-x_3 = x_30;
+x_2 = x_30;
 goto _start;
 }
 }
 }
 }
-}
 obj* l___private_init_lean_compiler_simpcase_2__addDefault(obj* x_0) {
 _start:
 {
@@ -349,7 +348,7 @@ lean::dec(x_0);
 return x_4;
 }
 }
-obj* l_Array_filterAux___main___at___private_init_lean_compiler_simpcase_3__mkCase___spec__1(obj* x_0, obj* x_1, obj* x_2) {
+obj* l_Array_filterAux___main___at___private_init_lean_compiler_simpcase_3__mkSimpCase___spec__1(obj* x_0, obj* x_1, obj* x_2) {
 _start:
 {
 obj* x_3; uint8 x_4; 
@@ -415,12 +414,12 @@ goto _start;
 }
 }
 }
-obj* l___private_init_lean_compiler_simpcase_3__mkCase(obj* x_0, obj* x_1, obj* x_2) {
+obj* l___private_init_lean_compiler_simpcase_3__mkSimpCase(obj* x_0, obj* x_1, obj* x_2) {
 _start:
 {
 obj* x_3; obj* x_4; obj* x_5; obj* x_6; uint8 x_7; 
 x_3 = lean::mk_nat_obj(0ul);
-x_4 = l_Array_filterAux___main___at___private_init_lean_compiler_simpcase_3__mkCase___spec__1(x_2, x_3, x_3);
+x_4 = l_Array_filterAux___main___at___private_init_lean_compiler_simpcase_3__mkSimpCase___spec__1(x_2, x_3, x_3);
 x_5 = l___private_init_lean_compiler_simpcase_2__addDefault(x_4);
 x_6 = lean::array_get_size(x_5);
 x_7 = lean::nat_dec_eq(x_6, x_3);
@@ -534,6 +533,90 @@ goto _start;
 }
 }
 }
+obj* _init_l_Array_hmmapAux___main___at_Lean_IR_FnBody_simpCase___main___spec__2___closed__1() {
+_start:
+{
+obj* x_0; obj* x_1; 
+x_0 = lean::box(12);
+x_1 = lean::alloc_cnstr(1, 1, 0);
+lean::cnstr_set(x_1, 0, x_0);
+return x_1;
+}
+}
+obj* l_Array_hmmapAux___main___at_Lean_IR_FnBody_simpCase___main___spec__2(obj* x_0, obj* x_1) {
+_start:
+{
+obj* x_2; uint8 x_3; 
+x_2 = lean::array_get_size(x_1);
+x_3 = lean::nat_dec_lt(x_0, x_2);
+lean::dec(x_2);
+if (x_3 == 0)
+{
+lean::dec(x_0);
+return x_1;
+}
+else
+{
+obj* x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_10; 
+x_6 = lean::array_fget(x_1, x_0);
+x_7 = l_Array_hmmapAux___main___at_Lean_IR_FnBody_simpCase___main___spec__2___closed__1;
+x_8 = lean::array_fset(x_1, x_0, x_7);
+x_9 = lean::mk_nat_obj(1ul);
+x_10 = lean::nat_add(x_0, x_9);
+if (lean::obj_tag(x_6) == 0)
+{
+obj* x_11; obj* x_13; obj* x_15; obj* x_16; obj* x_17; obj* x_18; 
+x_11 = lean::cnstr_get(x_6, 0);
+x_13 = lean::cnstr_get(x_6, 1);
+if (lean::is_exclusive(x_6)) {
+ x_15 = x_6;
+} else {
+ lean::inc(x_11);
+ lean::inc(x_13);
+ lean::dec(x_6);
+ x_15 = lean::box(0);
+}
+x_16 = l_Lean_IR_FnBody_simpCase___main(x_13);
+if (lean::is_scalar(x_15)) {
+ x_17 = lean::alloc_cnstr(0, 2, 0);
+} else {
+ x_17 = x_15;
+}
+lean::cnstr_set(x_17, 0, x_11);
+lean::cnstr_set(x_17, 1, x_16);
+x_18 = lean::array_fset(x_8, x_0, x_17);
+lean::dec(x_0);
+x_0 = x_10;
+x_1 = x_18;
+goto _start;
+}
+else
+{
+obj* x_21; obj* x_23; obj* x_24; obj* x_25; obj* x_26; 
+x_21 = lean::cnstr_get(x_6, 0);
+if (lean::is_exclusive(x_6)) {
+ x_23 = x_6;
+} else {
+ lean::inc(x_21);
+ lean::dec(x_6);
+ x_23 = lean::box(0);
+}
+x_24 = l_Lean_IR_FnBody_simpCase___main(x_21);
+if (lean::is_scalar(x_23)) {
+ x_25 = lean::alloc_cnstr(1, 1, 0);
+} else {
+ x_25 = x_23;
+}
+lean::cnstr_set(x_25, 0, x_24);
+x_26 = lean::array_fset(x_8, x_0, x_25);
+lean::dec(x_0);
+x_0 = x_10;
+x_1 = x_26;
+goto _start;
+}
+}
+}
+}
 obj* l_Lean_IR_FnBody_simpCase___main(obj* x_0) {
 _start:
 {
@@ -549,35 +632,24 @@ x_8 = l_Array_hmmapAux___main___at_Lean_IR_FnBody_simpCase___main___spec__1(x_7,
 switch (lean::obj_tag(x_4)) {
 case 9:
 {
-obj* x_9; obj* x_11; obj* x_13; obj* x_15; obj* x_16; obj* x_17; 
+obj* x_9; obj* x_11; obj* x_13; obj* x_16; obj* x_17; obj* x_18; 
 x_9 = lean::cnstr_get(x_4, 0);
+lean::inc(x_9);
 x_11 = lean::cnstr_get(x_4, 1);
+lean::inc(x_11);
 x_13 = lean::cnstr_get(x_4, 2);
-if (lean::is_exclusive(x_4)) {
- x_15 = x_4;
-} else {
- lean::inc(x_9);
- lean::inc(x_11);
- lean::inc(x_13);
- lean::dec(x_4);
- x_15 = lean::box(0);
-}
-if (lean::is_scalar(x_15)) {
- x_16 = lean::alloc_cnstr(9, 3, 0);
-} else {
- x_16 = x_15;
-}
-lean::cnstr_set(x_16, 0, x_9);
-lean::cnstr_set(x_16, 1, x_11);
-lean::cnstr_set(x_16, 2, x_13);
-x_17 = l_Lean_IR_reshape(x_8, x_16);
-return x_17;
+lean::inc(x_13);
+lean::dec(x_4);
+x_16 = l_Array_hmmapAux___main___at_Lean_IR_FnBody_simpCase___main___spec__2(x_7, x_13);
+x_17 = l___private_init_lean_compiler_simpcase_3__mkSimpCase(x_9, x_11, x_16);
+x_18 = l_Lean_IR_reshape(x_8, x_17);
+return x_18;
 }
 default:
 {
-obj* x_18; 
-x_18 = l_Lean_IR_reshape(x_8, x_4);
-return x_18;
+obj* x_19; 
+x_19 = l_Lean_IR_reshape(x_8, x_4);
+return x_19;
 }
 }
 }
@@ -628,9 +700,7 @@ return x_0;
 }
 }
 }
-namespace lean {
-namespace ir {
-obj* decl_simp_case_core(obj* x_0) {
+obj* l_Lean_IR_Decl_simpCase(obj* x_0) {
 _start:
 {
 obj* x_1; 
@@ -638,7 +708,6 @@ x_1 = l_Lean_IR_Decl_simpCase___main(x_0);
 return x_1;
 }
 }
-}}
 obj* initialize_init_default(obj*);
 obj* initialize_init_lean_compiler_ir(obj*);
 static bool _G_initialized = false;
@@ -650,5 +719,7 @@ w = initialize_init_default(w);
 if (io_result_is_error(w)) return w;
 w = initialize_init_lean_compiler_ir(w);
 if (io_result_is_error(w)) return w;
+ l_Array_hmmapAux___main___at_Lean_IR_FnBody_simpCase___main___spec__2___closed__1 = _init_l_Array_hmmapAux___main___at_Lean_IR_FnBody_simpCase___main___spec__2___closed__1();
+lean::mark_persistent(l_Array_hmmapAux___main___at_Lean_IR_FnBody_simpCase___main___spec__2___closed__1);
 return w;
 }