From e52e787ad5935db2a8ebbf45590fbbd49c1597ea Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 1 May 2019 21:01:03 -0700
Subject: [PATCH] fix(library/init/lean/compiler/pushproj): bug and cleanup

---
 library/init/data/array/basic.lean         |    2 +-
 library/init/lean/compiler/default.lean    |    2 +-
 library/init/lean/compiler/pushproj.lean   |   32 +-
 src/library/compiler/ir.cpp                |    5 +
 src/library/compiler/ir.h                  |    1 +
 src/library/compiler/llnf.cpp              |    3 +
 src/stage0/init/lean/compiler/pushproj.cpp | 1440 ++------------------
 7 files changed, 133 insertions(+), 1352 deletions(-)

diff --git a/library/init/data/array/basic.lean b/library/init/data/array/basic.lean
index 089aaf1920..d328525642 100644
--- a/library/init/data/array/basic.lean
+++ b/library/init/data/array/basic.lean
@@ -295,7 +295,7 @@ let r : Array α := mkEmpty (e - b) in
 if h : e ≤ a.size then extractAux a b e h r
 else r
 
-@[inline] protected def append (a : Array α) (b : Array α) : Array α :=
+protected def append (a : Array α) (b : Array α) : Array α :=
 b.foldl (λ a v, a.push v) a
 
 instance : HasAppend (Array α) := ⟨Array.append⟩
diff --git a/library/init/lean/compiler/default.lean b/library/init/lean/compiler/default.lean
index c63f04bbcc..960e022875 100644
--- a/library/init/lean/compiler/default.lean
+++ b/library/init/lean/compiler/default.lean
@@ -5,4 +5,4 @@ Authors: Leonardo de Moura
 -/
 prelude
 import init.lean.compiler.constfolding
-import init.lean.compiler.ir
+import init.lean.compiler.ir init.lean.compiler.pushproj
diff --git a/library/init/lean/compiler/pushproj.lean b/library/init/lean/compiler/pushproj.lean
index 8785eca068..121292e68c 100644
--- a/library/init/lean/compiler/pushproj.lean
+++ b/library/init/lean/compiler/pushproj.lean
@@ -9,27 +9,29 @@ namespace Lean
 namespace IR
 
 partial def pushProjs : Array FnBody → Array Alt → Array VarIdxSet → Array FnBody → VarIdxSet → Array FnBody × Array Alt
-| bs alts fvs ps psvs :=
+| bs alts afvs ps vs :=
   if bs.isEmpty then (ps.reverse, alts)
   else
-    let b  := bs.back in
-    let bs := bs.pop in
+    let b    := bs.back in
+    let bs   := bs.pop in
+    let done := λ _ : Unit, ((bs.push b) ++ ps.reverse, alts) in
+    let skip := λ _ : Unit, pushProjs bs alts afvs (ps.push b) (b.collectFreeVars vs) in
     match b with
     | FnBody.vdecl x t v _ :=
       (match v with
        | Expr.proj _ _    :=
-         if !psvs.contains x.idx && !fvs.all (λ s, s.contains x.idx) then
+         if !vs.contains x.idx && !afvs.all (λ s, s.contains x.idx) then
            let alts := alts.hmapIdx $ λ i alt, alt.modifyBody $ λ b',
-              if (fvs.get i).contains x.idx then b.setBody b'
+              if (afvs.get i).contains x.idx then b.setBody b'
               else b' in
-           let fvs  := fvs.hmap $ λ s, if s.contains x.idx then b.collectFreeVars s else s in
-           pushProjs bs alts fvs ps psvs
+           let fvs  := afvs.hmap $ λ s, if s.contains x.idx then b.collectFreeVars s else s in
+           pushProjs bs alts fvs ps vs
          else
-           pushProjs bs alts fvs (ps.push b) (b.collectFreeVars psvs)
-       | Expr.uproj _ _   := pushProjs bs alts fvs (ps.push b) (b.collectFreeVars psvs)
-       | Expr.sproj _ _ _ := pushProjs bs alts fvs (ps.push b) (b.collectFreeVars psvs)
-       | other            := ((bs.push b) ++ ps.reverse, alts))
-    | other := ((bs.push b) ++ ps.reverse, alts)
+           skip ()
+       | Expr.uproj _ _   := skip ()
+       | Expr.sproj _ _ _ := skip ()
+       | _                := done ())
+    | _ := done ()
 
 /-- Push projections inside `cases` branches. -/
 partial def FnBody.pushProj : FnBody → FnBody
@@ -37,8 +39,10 @@ partial def FnBody.pushProj : FnBody → FnBody
   let (bs, term) := b.flatten in
   match term with
   | FnBody.case tid x alts :=
-    let fvs        := alts.map $ λ alt, alt.body.freeVars in
-    let (bs, alts) := pushProjs bs alts fvs Array.empty {} in
+    let afvs       := alts.map $ λ alt, alt.body.freeVars in
+    let vs         := ({} : VarIdxSet) in
+    let vs         := vs.insert x.idx in
+    let (bs, alts) := pushProjs bs alts afvs Array.empty vs in
     let alts       := alts.hmap $ λ alt, alt.modifyBody $ λ b, FnBody.pushProj b in
     let term       := FnBody.case tid x alts in
     reshape bs term
diff --git a/src/library/compiler/ir.cpp b/src/library/compiler/ir.cpp
index 5f76560b77..3376a2e4b4 100644
--- a/src/library/compiler/ir.cpp
+++ b/src/library/compiler/ir.cpp
@@ -38,6 +38,7 @@ object * mk_alt_core(object * n, object * cidx, object * size, object * usize, o
 object * mk_decl_core(object * f, object * xs, uint8 ty, object * b);
 object * decl_to_string_core(object * d);
 object * decl_max_var_core(object * d);
+object * decl_push_proj_core(object * d);
 /*
 inductive IRType
 | float | uint8 | uint16 | uint32 | uint64 | usize
@@ -118,6 +119,10 @@ nat decl_max_var(decl const & d) {
     inc(d.raw());
     return nat(decl_max_var_core(d.raw()));
 }
+decl decl_push_proj(decl const & d) {
+    inc(d.raw());
+    return decl(decl_push_proj_core(d.raw()));
+}
 }
 
 class to_ir_fn {
diff --git a/src/library/compiler/ir.h b/src/library/compiler/ir.h
index 2329c354ed..2b62886cea 100644
--- a/src/library/compiler/ir.h
+++ b/src/library/compiler/ir.h
@@ -12,6 +12,7 @@ namespace ir {
 typedef object_ref decl;
 std::string decl_to_string(decl const & d);
 nat decl_max_var(decl const & d);
+decl decl_push_proj(decl const & d);
 }
 ir::decl to_ir_decl(environment const & env, comp_decl const & d);
 }
diff --git a/src/library/compiler/llnf.cpp b/src/library/compiler/llnf.cpp
index f5351dd067..2eabd8cbc8 100644
--- a/src/library/compiler/llnf.cpp
+++ b/src/library/compiler/llnf.cpp
@@ -2419,6 +2419,9 @@ static void display_ir(environment const & env, comp_decl const & decl) {
     ir::decl d = to_ir_decl(env, decl);
     tout() << ir::decl_to_string(d) << "\n";
     tout() << "Max var: " << ir::decl_max_var(d).to_std_string() << "\n";
+    tout() << "after push proj\n";
+    d = ir::decl_push_proj(d);
+    tout() << ir::decl_to_string(d) << "\n";
 }
 
 pair<environment, comp_decls> to_llnf(environment const & env, comp_decls const & ds, bool unboxed) {
diff --git a/src/stage0/init/lean/compiler/pushproj.cpp b/src/stage0/init/lean/compiler/pushproj.cpp
index 7163d3754a..8bb6152f1e 100644
--- a/src/stage0/init/lean/compiler/pushproj.cpp
+++ b/src/stage0/init/lean/compiler/pushproj.cpp
@@ -14,96 +14,51 @@ typedef lean::uint32 uint32; typedef lean::uint64 uint64;
 #pragma GCC diagnostic ignored "-Wunused-label"
 #pragma GCC diagnostic ignored "-Wunused-but-set-variable"
 #endif
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__16___boxed(obj*, obj*, obj*, obj*);
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__13(obj*, obj*, obj*, obj*);
+obj* l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__3(obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_IR_FnBody_collectFreeVars(obj*, obj*);
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__14___boxed(obj*, obj*, obj*, obj*);
 extern obj* l_Array_empty___closed__1;
 namespace lean {
 obj* nat_sub(obj*, obj*);
 }
 extern obj* l_Lean_IR_vsetInh;
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__17___boxed(obj*, obj*, obj*, obj*);
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__22(obj*, obj*, obj*, obj*);
 namespace lean {
 namespace ir {
 obj* decl_push_proj_core(obj*);
 }}
-obj* l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__7(obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_IR_pushProjs___main___closed__1;
 obj* l_Array_miterateAux___main___at_Lean_IR_FnBody_pushProj___main___spec__1___boxed(obj*, obj*, obj*, obj*);
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__15___boxed(obj*, obj*, obj*, obj*);
 obj* l_Array_hmmapAux___main___at_Lean_IR_FnBody_pushProj___main___spec__2(obj*, obj*);
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__22___boxed(obj*, obj*, obj*, obj*);
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__24___boxed(obj*, obj*, obj*, obj*);
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__3___boxed(obj*, obj*, obj*, obj*);
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__9___boxed(obj*, obj*, obj*, obj*);
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__18___boxed(obj*, obj*, obj*, obj*);
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__24(obj*, obj*, obj*, obj*);
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__25(obj*, obj*, obj*, obj*);
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__2(obj*, obj*, obj*, obj*);
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__4___boxed(obj*, obj*, obj*, obj*);
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__19___boxed(obj*, obj*, obj*, obj*);
+obj* l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__4___boxed(obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_IR_Decl_pushProj___main(obj*);
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__23___boxed(obj*, obj*, obj*, obj*);
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__21(obj*, obj*, obj*, obj*);
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__20(obj*, obj*, obj*, obj*);
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__27(obj*, obj*, obj*, obj*);
 obj* l_Lean_IR_FnBody_freeVars(obj*);
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__23(obj*, obj*, obj*, obj*);
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__8(obj*, obj*, obj*, obj*);
 obj* l_Lean_IR_reshape(obj*, obj*);
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__25___boxed(obj*, obj*, obj*, obj*);
+uint8 l_Array_anyAux___main___at_Lean_IR_pushProjs___main___spec__2(obj*, obj*, obj*, obj*);
 obj* l_Lean_IR_FnBody_pushProj(obj*);
-obj* l_Array_anyAux___main___at_Lean_IR_pushProjs___main___spec__5___boxed(obj*, obj*, obj*, obj*);
 namespace lean {
 uint8 nat_dec_lt(obj*, obj*);
 }
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__21___boxed(obj*, obj*, obj*, 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 {
 obj* nat_add(obj*, obj*);
 }
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__26___boxed(obj*, obj*, obj*, obj*);
 uint8 l_Array_isEmpty___rarg(obj*);
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__17(obj*, obj*, obj*, obj*);
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__3(obj*, obj*, obj*, obj*);
 obj* l_Lean_IR_pushProjs(obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_IR_FnBody_pushProj___main(obj*);
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__18(obj*, obj*, obj*, obj*);
-obj* l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__6___closed__1;
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__4(obj*, obj*, obj*, obj*);
-obj* l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__7___boxed(obj*, obj*, obj*, obj*, obj*);
 obj* l_Nat_decLt___boxed(obj*, obj*);
 obj* l_Array_reverseAux___main___rarg(obj*, obj*);
 obj* l_Lean_IR_AltCore_body___main(obj*);
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__19(obj*, obj*, obj*, obj*);
 obj* l_Lean_IR_pushProjs___main(obj*, obj*, obj*, obj*, obj*);
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__8___boxed(obj*, obj*, obj*, obj*);
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__14(obj*, obj*, obj*, obj*);
 obj* l_Array_back___at_Lean_IR_pushProjs___main___spec__1(obj*);
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__2___boxed(obj*, obj*, obj*, obj*);
-obj* l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__6(obj*, obj*, obj*, obj*, obj*, obj*);
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__10___boxed(obj*, obj*, obj*, obj*);
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__15(obj*, obj*, obj*, obj*);
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__20___boxed(obj*, obj*, obj*, obj*);
 obj* l_Lean_IR_FnBody_setBody___main(obj*, obj*);
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__11___boxed(obj*, obj*, obj*, obj*);
-obj* l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__6___boxed(obj*, obj*, obj*, obj*, obj*, obj*);
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__16(obj*, obj*, obj*, obj*);
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__10(obj*, obj*, obj*, obj*);
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__9(obj*, obj*, obj*, obj*);
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__11(obj*, obj*, obj*, obj*);
+obj* l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__4(obj*, obj*, obj*, obj*, obj*);
+obj* l_Array_anyAux___main___at_Lean_IR_pushProjs___main___spec__2___boxed(obj*, obj*, obj*, obj*);
 obj* l_Array_back___at_Lean_IR_pushProjs___main___spec__1___boxed(obj*);
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__12___boxed(obj*, obj*, obj*, obj*);
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__26(obj*, obj*, obj*, obj*);
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__12(obj*, obj*, obj*, obj*);
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__13___boxed(obj*, obj*, obj*, obj*);
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__27___boxed(obj*, obj*, obj*, obj*);
+obj* l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__3___closed__1;
+obj* l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__3___boxed(obj*, obj*, obj*, obj*, obj*, obj*);
+obj* l_Array_miterateAux___main___at_Array_append___spec__1___rarg(obj*, obj*, obj*, obj*);
 obj* l_Array_miterateAux___main___at_Lean_IR_FnBody_pushProj___main___spec__1(obj*, obj*, obj*, obj*);
 extern obj* l_Lean_IR_Inhabited;
-uint8 l_Array_anyAux___main___at_Lean_IR_pushProjs___main___spec__5(obj*, obj*, obj*, obj*);
 obj* l_Array_back___at_Lean_IR_pushProjs___main___spec__1(obj* x_0) {
 _start:
 {
@@ -118,85 +73,7 @@ lean::dec(x_3);
 return x_6;
 }
 }
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__2(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; uint8 x_5; 
-x_4 = lean::array_get_size(x_1);
-x_5 = lean::nat_dec_lt(x_2, x_4);
-lean::dec(x_4);
-if (x_5 == 0)
-{
-lean::dec(x_2);
-return x_3;
-}
-else
-{
-obj* x_8; obj* x_9; obj* x_10; obj* x_11; 
-x_8 = lean::array_index(x_1, x_2);
-x_9 = lean::array_push(x_3, x_8);
-x_10 = lean::mk_nat_obj(1ul);
-x_11 = lean::nat_add(x_2, x_10);
-lean::dec(x_2);
-x_2 = x_11;
-x_3 = x_9;
-goto _start;
-}
-}
-}
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__3(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; uint8 x_5; 
-x_4 = lean::array_get_size(x_1);
-x_5 = lean::nat_dec_lt(x_2, x_4);
-lean::dec(x_4);
-if (x_5 == 0)
-{
-lean::dec(x_2);
-return x_3;
-}
-else
-{
-obj* x_8; obj* x_9; obj* x_10; obj* x_11; 
-x_8 = lean::array_index(x_1, x_2);
-x_9 = lean::array_push(x_3, x_8);
-x_10 = lean::mk_nat_obj(1ul);
-x_11 = lean::nat_add(x_2, x_10);
-lean::dec(x_2);
-x_2 = x_11;
-x_3 = x_9;
-goto _start;
-}
-}
-}
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__4(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; uint8 x_5; 
-x_4 = lean::array_get_size(x_1);
-x_5 = lean::nat_dec_lt(x_2, x_4);
-lean::dec(x_4);
-if (x_5 == 0)
-{
-lean::dec(x_2);
-return x_3;
-}
-else
-{
-obj* x_8; obj* x_9; obj* x_10; obj* x_11; 
-x_8 = lean::array_index(x_1, x_2);
-x_9 = lean::array_push(x_3, x_8);
-x_10 = lean::mk_nat_obj(1ul);
-x_11 = lean::nat_add(x_2, x_10);
-lean::dec(x_2);
-x_2 = x_11;
-x_3 = x_9;
-goto _start;
-}
-}
-}
-uint8 l_Array_anyAux___main___at_Lean_IR_pushProjs___main___spec__5(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
+uint8 l_Array_anyAux___main___at_Lean_IR_pushProjs___main___spec__2(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
 _start:
 {
 obj* x_4; uint8 x_5; 
@@ -235,7 +112,7 @@ goto _start;
 }
 }
 }
-obj* _init_l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__6___closed__1() {
+obj* _init_l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__3___closed__1() {
 _start:
 {
 obj* x_0; obj* x_1; 
@@ -245,7 +122,7 @@ lean::cnstr_set(x_1, 0, x_0);
 return x_1;
 }
 }
-obj* l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__6(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
+obj* l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__3(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
 _start:
 {
 obj* x_6; uint8 x_7; 
@@ -262,7 +139,7 @@ else
 {
 obj* x_11; obj* x_12; obj* x_13; obj* x_14; obj* x_15; 
 x_11 = lean::array_index(x_5, x_4);
-x_12 = l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__6___closed__1;
+x_12 = l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__3___closed__1;
 x_13 = lean::array_update(x_5, x_4, x_12);
 x_14 = lean::mk_nat_obj(1ul);
 x_15 = lean::nat_add(x_4, x_14);
@@ -372,7 +249,7 @@ goto _start;
 }
 }
 }
-obj* l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__7(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
+obj* l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__4(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
 _start:
 {
 obj* x_5; uint8 x_6; 
@@ -419,526 +296,6 @@ goto _start;
 }
 }
 }
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__8(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; uint8 x_5; 
-x_4 = lean::array_get_size(x_1);
-x_5 = lean::nat_dec_lt(x_2, x_4);
-lean::dec(x_4);
-if (x_5 == 0)
-{
-lean::dec(x_2);
-return x_3;
-}
-else
-{
-obj* x_8; obj* x_9; obj* x_10; obj* x_11; 
-x_8 = lean::array_index(x_1, x_2);
-x_9 = lean::array_push(x_3, x_8);
-x_10 = lean::mk_nat_obj(1ul);
-x_11 = lean::nat_add(x_2, x_10);
-lean::dec(x_2);
-x_2 = x_11;
-x_3 = x_9;
-goto _start;
-}
-}
-}
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__9(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; uint8 x_5; 
-x_4 = lean::array_get_size(x_1);
-x_5 = lean::nat_dec_lt(x_2, x_4);
-lean::dec(x_4);
-if (x_5 == 0)
-{
-lean::dec(x_2);
-return x_3;
-}
-else
-{
-obj* x_8; obj* x_9; obj* x_10; obj* x_11; 
-x_8 = lean::array_index(x_1, x_2);
-x_9 = lean::array_push(x_3, x_8);
-x_10 = lean::mk_nat_obj(1ul);
-x_11 = lean::nat_add(x_2, x_10);
-lean::dec(x_2);
-x_2 = x_11;
-x_3 = x_9;
-goto _start;
-}
-}
-}
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__10(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; uint8 x_5; 
-x_4 = lean::array_get_size(x_1);
-x_5 = lean::nat_dec_lt(x_2, x_4);
-lean::dec(x_4);
-if (x_5 == 0)
-{
-lean::dec(x_2);
-return x_3;
-}
-else
-{
-obj* x_8; obj* x_9; obj* x_10; obj* x_11; 
-x_8 = lean::array_index(x_1, x_2);
-x_9 = lean::array_push(x_3, x_8);
-x_10 = lean::mk_nat_obj(1ul);
-x_11 = lean::nat_add(x_2, x_10);
-lean::dec(x_2);
-x_2 = x_11;
-x_3 = x_9;
-goto _start;
-}
-}
-}
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__11(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; uint8 x_5; 
-x_4 = lean::array_get_size(x_1);
-x_5 = lean::nat_dec_lt(x_2, x_4);
-lean::dec(x_4);
-if (x_5 == 0)
-{
-lean::dec(x_2);
-return x_3;
-}
-else
-{
-obj* x_8; obj* x_9; obj* x_10; obj* x_11; 
-x_8 = lean::array_index(x_1, x_2);
-x_9 = lean::array_push(x_3, x_8);
-x_10 = lean::mk_nat_obj(1ul);
-x_11 = lean::nat_add(x_2, x_10);
-lean::dec(x_2);
-x_2 = x_11;
-x_3 = x_9;
-goto _start;
-}
-}
-}
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__12(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; uint8 x_5; 
-x_4 = lean::array_get_size(x_1);
-x_5 = lean::nat_dec_lt(x_2, x_4);
-lean::dec(x_4);
-if (x_5 == 0)
-{
-lean::dec(x_2);
-return x_3;
-}
-else
-{
-obj* x_8; obj* x_9; obj* x_10; obj* x_11; 
-x_8 = lean::array_index(x_1, x_2);
-x_9 = lean::array_push(x_3, x_8);
-x_10 = lean::mk_nat_obj(1ul);
-x_11 = lean::nat_add(x_2, x_10);
-lean::dec(x_2);
-x_2 = x_11;
-x_3 = x_9;
-goto _start;
-}
-}
-}
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__13(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; uint8 x_5; 
-x_4 = lean::array_get_size(x_1);
-x_5 = lean::nat_dec_lt(x_2, x_4);
-lean::dec(x_4);
-if (x_5 == 0)
-{
-lean::dec(x_2);
-return x_3;
-}
-else
-{
-obj* x_8; obj* x_9; obj* x_10; obj* x_11; 
-x_8 = lean::array_index(x_1, x_2);
-x_9 = lean::array_push(x_3, x_8);
-x_10 = lean::mk_nat_obj(1ul);
-x_11 = lean::nat_add(x_2, x_10);
-lean::dec(x_2);
-x_2 = x_11;
-x_3 = x_9;
-goto _start;
-}
-}
-}
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__14(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; uint8 x_5; 
-x_4 = lean::array_get_size(x_1);
-x_5 = lean::nat_dec_lt(x_2, x_4);
-lean::dec(x_4);
-if (x_5 == 0)
-{
-lean::dec(x_2);
-return x_3;
-}
-else
-{
-obj* x_8; obj* x_9; obj* x_10; obj* x_11; 
-x_8 = lean::array_index(x_1, x_2);
-x_9 = lean::array_push(x_3, x_8);
-x_10 = lean::mk_nat_obj(1ul);
-x_11 = lean::nat_add(x_2, x_10);
-lean::dec(x_2);
-x_2 = x_11;
-x_3 = x_9;
-goto _start;
-}
-}
-}
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__15(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; uint8 x_5; 
-x_4 = lean::array_get_size(x_1);
-x_5 = lean::nat_dec_lt(x_2, x_4);
-lean::dec(x_4);
-if (x_5 == 0)
-{
-lean::dec(x_2);
-return x_3;
-}
-else
-{
-obj* x_8; obj* x_9; obj* x_10; obj* x_11; 
-x_8 = lean::array_index(x_1, x_2);
-x_9 = lean::array_push(x_3, x_8);
-x_10 = lean::mk_nat_obj(1ul);
-x_11 = lean::nat_add(x_2, x_10);
-lean::dec(x_2);
-x_2 = x_11;
-x_3 = x_9;
-goto _start;
-}
-}
-}
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__16(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; uint8 x_5; 
-x_4 = lean::array_get_size(x_1);
-x_5 = lean::nat_dec_lt(x_2, x_4);
-lean::dec(x_4);
-if (x_5 == 0)
-{
-lean::dec(x_2);
-return x_3;
-}
-else
-{
-obj* x_8; obj* x_9; obj* x_10; obj* x_11; 
-x_8 = lean::array_index(x_1, x_2);
-x_9 = lean::array_push(x_3, x_8);
-x_10 = lean::mk_nat_obj(1ul);
-x_11 = lean::nat_add(x_2, x_10);
-lean::dec(x_2);
-x_2 = x_11;
-x_3 = x_9;
-goto _start;
-}
-}
-}
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__17(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; uint8 x_5; 
-x_4 = lean::array_get_size(x_1);
-x_5 = lean::nat_dec_lt(x_2, x_4);
-lean::dec(x_4);
-if (x_5 == 0)
-{
-lean::dec(x_2);
-return x_3;
-}
-else
-{
-obj* x_8; obj* x_9; obj* x_10; obj* x_11; 
-x_8 = lean::array_index(x_1, x_2);
-x_9 = lean::array_push(x_3, x_8);
-x_10 = lean::mk_nat_obj(1ul);
-x_11 = lean::nat_add(x_2, x_10);
-lean::dec(x_2);
-x_2 = x_11;
-x_3 = x_9;
-goto _start;
-}
-}
-}
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__18(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; uint8 x_5; 
-x_4 = lean::array_get_size(x_1);
-x_5 = lean::nat_dec_lt(x_2, x_4);
-lean::dec(x_4);
-if (x_5 == 0)
-{
-lean::dec(x_2);
-return x_3;
-}
-else
-{
-obj* x_8; obj* x_9; obj* x_10; obj* x_11; 
-x_8 = lean::array_index(x_1, x_2);
-x_9 = lean::array_push(x_3, x_8);
-x_10 = lean::mk_nat_obj(1ul);
-x_11 = lean::nat_add(x_2, x_10);
-lean::dec(x_2);
-x_2 = x_11;
-x_3 = x_9;
-goto _start;
-}
-}
-}
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__19(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; uint8 x_5; 
-x_4 = lean::array_get_size(x_1);
-x_5 = lean::nat_dec_lt(x_2, x_4);
-lean::dec(x_4);
-if (x_5 == 0)
-{
-lean::dec(x_2);
-return x_3;
-}
-else
-{
-obj* x_8; obj* x_9; obj* x_10; obj* x_11; 
-x_8 = lean::array_index(x_1, x_2);
-x_9 = lean::array_push(x_3, x_8);
-x_10 = lean::mk_nat_obj(1ul);
-x_11 = lean::nat_add(x_2, x_10);
-lean::dec(x_2);
-x_2 = x_11;
-x_3 = x_9;
-goto _start;
-}
-}
-}
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__20(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; uint8 x_5; 
-x_4 = lean::array_get_size(x_1);
-x_5 = lean::nat_dec_lt(x_2, x_4);
-lean::dec(x_4);
-if (x_5 == 0)
-{
-lean::dec(x_2);
-return x_3;
-}
-else
-{
-obj* x_8; obj* x_9; obj* x_10; obj* x_11; 
-x_8 = lean::array_index(x_1, x_2);
-x_9 = lean::array_push(x_3, x_8);
-x_10 = lean::mk_nat_obj(1ul);
-x_11 = lean::nat_add(x_2, x_10);
-lean::dec(x_2);
-x_2 = x_11;
-x_3 = x_9;
-goto _start;
-}
-}
-}
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__21(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; uint8 x_5; 
-x_4 = lean::array_get_size(x_1);
-x_5 = lean::nat_dec_lt(x_2, x_4);
-lean::dec(x_4);
-if (x_5 == 0)
-{
-lean::dec(x_2);
-return x_3;
-}
-else
-{
-obj* x_8; obj* x_9; obj* x_10; obj* x_11; 
-x_8 = lean::array_index(x_1, x_2);
-x_9 = lean::array_push(x_3, x_8);
-x_10 = lean::mk_nat_obj(1ul);
-x_11 = lean::nat_add(x_2, x_10);
-lean::dec(x_2);
-x_2 = x_11;
-x_3 = x_9;
-goto _start;
-}
-}
-}
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__22(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; uint8 x_5; 
-x_4 = lean::array_get_size(x_1);
-x_5 = lean::nat_dec_lt(x_2, x_4);
-lean::dec(x_4);
-if (x_5 == 0)
-{
-lean::dec(x_2);
-return x_3;
-}
-else
-{
-obj* x_8; obj* x_9; obj* x_10; obj* x_11; 
-x_8 = lean::array_index(x_1, x_2);
-x_9 = lean::array_push(x_3, x_8);
-x_10 = lean::mk_nat_obj(1ul);
-x_11 = lean::nat_add(x_2, x_10);
-lean::dec(x_2);
-x_2 = x_11;
-x_3 = x_9;
-goto _start;
-}
-}
-}
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__23(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; uint8 x_5; 
-x_4 = lean::array_get_size(x_1);
-x_5 = lean::nat_dec_lt(x_2, x_4);
-lean::dec(x_4);
-if (x_5 == 0)
-{
-lean::dec(x_2);
-return x_3;
-}
-else
-{
-obj* x_8; obj* x_9; obj* x_10; obj* x_11; 
-x_8 = lean::array_index(x_1, x_2);
-x_9 = lean::array_push(x_3, x_8);
-x_10 = lean::mk_nat_obj(1ul);
-x_11 = lean::nat_add(x_2, x_10);
-lean::dec(x_2);
-x_2 = x_11;
-x_3 = x_9;
-goto _start;
-}
-}
-}
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__24(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; uint8 x_5; 
-x_4 = lean::array_get_size(x_1);
-x_5 = lean::nat_dec_lt(x_2, x_4);
-lean::dec(x_4);
-if (x_5 == 0)
-{
-lean::dec(x_2);
-return x_3;
-}
-else
-{
-obj* x_8; obj* x_9; obj* x_10; obj* x_11; 
-x_8 = lean::array_index(x_1, x_2);
-x_9 = lean::array_push(x_3, x_8);
-x_10 = lean::mk_nat_obj(1ul);
-x_11 = lean::nat_add(x_2, x_10);
-lean::dec(x_2);
-x_2 = x_11;
-x_3 = x_9;
-goto _start;
-}
-}
-}
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__25(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; uint8 x_5; 
-x_4 = lean::array_get_size(x_1);
-x_5 = lean::nat_dec_lt(x_2, x_4);
-lean::dec(x_4);
-if (x_5 == 0)
-{
-lean::dec(x_2);
-return x_3;
-}
-else
-{
-obj* x_8; obj* x_9; obj* x_10; obj* x_11; 
-x_8 = lean::array_index(x_1, x_2);
-x_9 = lean::array_push(x_3, x_8);
-x_10 = lean::mk_nat_obj(1ul);
-x_11 = lean::nat_add(x_2, x_10);
-lean::dec(x_2);
-x_2 = x_11;
-x_3 = x_9;
-goto _start;
-}
-}
-}
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__26(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; uint8 x_5; 
-x_4 = lean::array_get_size(x_1);
-x_5 = lean::nat_dec_lt(x_2, x_4);
-lean::dec(x_4);
-if (x_5 == 0)
-{
-lean::dec(x_2);
-return x_3;
-}
-else
-{
-obj* x_8; obj* x_9; obj* x_10; obj* x_11; 
-x_8 = lean::array_index(x_1, x_2);
-x_9 = lean::array_push(x_3, x_8);
-x_10 = lean::mk_nat_obj(1ul);
-x_11 = lean::nat_add(x_2, x_10);
-lean::dec(x_2);
-x_2 = x_11;
-x_3 = x_9;
-goto _start;
-}
-}
-}
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__27(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; uint8 x_5; 
-x_4 = lean::array_get_size(x_1);
-x_5 = lean::nat_dec_lt(x_2, x_4);
-lean::dec(x_4);
-if (x_5 == 0)
-{
-lean::dec(x_2);
-return x_3;
-}
-else
-{
-obj* x_8; obj* x_9; obj* x_10; obj* x_11; 
-x_8 = lean::array_index(x_1, x_2);
-x_9 = lean::array_push(x_3, x_8);
-x_10 = lean::mk_nat_obj(1ul);
-x_11 = lean::nat_add(x_2, x_10);
-lean::dec(x_2);
-x_2 = x_11;
-x_3 = x_9;
-goto _start;
-}
-}
-}
 obj* _init_l_Lean_IR_pushProjs___main___closed__1() {
 _start:
 {
@@ -964,489 +321,130 @@ obj* x_8;
 x_8 = lean::cnstr_get(x_6, 1);
 lean::inc(x_8);
 switch (lean::obj_tag(x_8)) {
-case 0:
-{
-obj* x_13; obj* x_14; obj* x_16; obj* x_17; obj* x_20; 
-lean::dec(x_4);
-lean::dec(x_8);
-lean::dec(x_2);
-x_13 = lean::array_push(x_7, x_6);
-x_14 = lean::mk_nat_obj(0ul);
-lean::inc(x_3);
-x_16 = l_Array_reverseAux___main___rarg(x_3, x_14);
-x_17 = l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__2(x_3, x_16, x_14, x_13);
-lean::dec(x_16);
-lean::dec(x_3);
-x_20 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_20, 0, x_17);
-lean::cnstr_set(x_20, 1, x_1);
-return x_20;
-}
-case 1:
-{
-obj* x_24; obj* x_25; obj* x_27; obj* x_28; obj* x_31; 
-lean::dec(x_4);
-lean::dec(x_8);
-lean::dec(x_2);
-x_24 = lean::array_push(x_7, x_6);
-x_25 = lean::mk_nat_obj(0ul);
-lean::inc(x_3);
-x_27 = l_Array_reverseAux___main___rarg(x_3, x_25);
-x_28 = l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__3(x_3, x_27, x_25, x_24);
-lean::dec(x_27);
-lean::dec(x_3);
-x_31 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_31, 0, x_28);
-lean::cnstr_set(x_31, 1, x_1);
-return x_31;
-}
-case 2:
-{
-obj* x_35; obj* x_36; obj* x_38; obj* x_39; obj* x_42; 
-lean::dec(x_4);
-lean::dec(x_8);
-lean::dec(x_2);
-x_35 = lean::array_push(x_7, x_6);
-x_36 = lean::mk_nat_obj(0ul);
-lean::inc(x_3);
-x_38 = l_Array_reverseAux___main___rarg(x_3, x_36);
-x_39 = l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__4(x_3, x_38, x_36, x_35);
-lean::dec(x_38);
-lean::dec(x_3);
-x_42 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_42, 0, x_39);
-lean::cnstr_set(x_42, 1, x_1);
-return x_42;
-}
 case 3:
 {
-obj* x_44; obj* x_47; 
+obj* x_11; obj* x_14; 
 lean::dec(x_8);
-x_44 = lean::cnstr_get(x_6, 0);
-lean::inc(x_44);
+x_11 = lean::cnstr_get(x_6, 0);
+lean::inc(x_11);
 lean::inc(x_4);
-x_47 = l_RBNode_findCore___main___at___private_init_lean_compiler_ir_2__collectIndex___spec__1(x_4, x_44);
-if (lean::obj_tag(x_47) == 0)
+x_14 = l_RBNode_findCore___main___at___private_init_lean_compiler_ir_2__collectIndex___spec__1(x_4, x_11);
+if (lean::obj_tag(x_14) == 0)
 {
-obj* x_48; obj* x_49; uint8 x_50; 
-x_48 = l_Lean_IR_pushProjs___main___closed__1;
-x_49 = lean::mk_nat_obj(0ul);
-x_50 = l_Array_anyAux___main___at_Lean_IR_pushProjs___main___spec__5(x_48, x_44, x_2, x_49);
-if (x_50 == 0)
+obj* x_15; obj* x_16; uint8 x_17; 
+x_15 = l_Lean_IR_pushProjs___main___closed__1;
+x_16 = lean::mk_nat_obj(0ul);
+x_17 = l_Array_anyAux___main___at_Lean_IR_pushProjs___main___spec__2(x_15, x_11, x_2, x_16);
+if (x_17 == 0)
 {
-obj* x_53; obj* x_54; 
-lean::dec(x_44);
+obj* x_20; obj* x_21; 
+lean::dec(x_11);
 lean::inc(x_6);
-x_53 = lean::array_push(x_3, x_6);
-x_54 = l_Lean_IR_FnBody_collectFreeVars(x_6, x_4);
+x_20 = lean::array_push(x_3, x_6);
+x_21 = l_Lean_IR_FnBody_collectFreeVars(x_6, x_4);
 x_0 = x_7;
-x_3 = x_53;
-x_4 = x_54;
+x_3 = x_20;
+x_4 = x_21;
 goto _start;
 }
 else
 {
-obj* x_57; obj* x_58; 
+obj* x_24; obj* x_25; 
 lean::inc(x_6);
-x_57 = l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__6(x_2, x_6, x_48, x_44, x_49, x_1);
-x_58 = l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__7(x_6, x_48, x_44, x_49, x_2);
-lean::dec(x_44);
+x_24 = l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__3(x_2, x_6, x_15, x_11, x_16, x_1);
+x_25 = l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__4(x_6, x_15, x_11, x_16, x_2);
+lean::dec(x_11);
 x_0 = x_7;
-x_1 = x_57;
-x_2 = x_58;
+x_1 = x_24;
+x_2 = x_25;
 goto _start;
 }
 }
 else
 {
-obj* x_64; obj* x_65; 
-lean::dec(x_44);
-lean::dec(x_47);
+obj* x_31; obj* x_32; 
+lean::dec(x_14);
+lean::dec(x_11);
 lean::inc(x_6);
-x_64 = lean::array_push(x_3, x_6);
-x_65 = l_Lean_IR_FnBody_collectFreeVars(x_6, x_4);
+x_31 = lean::array_push(x_3, x_6);
+x_32 = l_Lean_IR_FnBody_collectFreeVars(x_6, x_4);
 x_0 = x_7;
-x_3 = x_64;
-x_4 = x_65;
+x_3 = x_31;
+x_4 = x_32;
 goto _start;
 }
 }
-case 6:
-{
-obj* x_70; obj* x_71; obj* x_73; obj* x_74; obj* x_77; 
-lean::dec(x_4);
-lean::dec(x_8);
-lean::dec(x_2);
-x_70 = lean::array_push(x_7, x_6);
-x_71 = lean::mk_nat_obj(0ul);
-lean::inc(x_3);
-x_73 = l_Array_reverseAux___main___rarg(x_3, x_71);
-x_74 = l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__8(x_3, x_73, x_71, x_70);
-lean::dec(x_73);
-lean::dec(x_3);
-x_77 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_77, 0, x_74);
-lean::cnstr_set(x_77, 1, x_1);
-return x_77;
-}
-case 7:
-{
-obj* x_81; obj* x_82; obj* x_84; obj* x_85; obj* x_88; 
-lean::dec(x_4);
-lean::dec(x_8);
-lean::dec(x_2);
-x_81 = lean::array_push(x_7, x_6);
-x_82 = lean::mk_nat_obj(0ul);
-lean::inc(x_3);
-x_84 = l_Array_reverseAux___main___rarg(x_3, x_82);
-x_85 = l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__9(x_3, x_84, x_82, x_81);
-lean::dec(x_84);
-lean::dec(x_3);
-x_88 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_88, 0, x_85);
-lean::cnstr_set(x_88, 1, x_1);
-return x_88;
-}
-case 8:
-{
-obj* x_92; obj* x_93; obj* x_95; obj* x_96; obj* x_99; 
-lean::dec(x_4);
-lean::dec(x_8);
-lean::dec(x_2);
-x_92 = lean::array_push(x_7, x_6);
-x_93 = lean::mk_nat_obj(0ul);
-lean::inc(x_3);
-x_95 = l_Array_reverseAux___main___rarg(x_3, x_93);
-x_96 = l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__10(x_3, x_95, x_93, x_92);
-lean::dec(x_95);
-lean::dec(x_3);
-x_99 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_99, 0, x_96);
-lean::cnstr_set(x_99, 1, x_1);
-return x_99;
-}
-case 9:
-{
-obj* x_103; obj* x_104; obj* x_106; obj* x_107; obj* x_110; 
-lean::dec(x_4);
-lean::dec(x_8);
-lean::dec(x_2);
-x_103 = lean::array_push(x_7, x_6);
-x_104 = lean::mk_nat_obj(0ul);
-lean::inc(x_3);
-x_106 = l_Array_reverseAux___main___rarg(x_3, x_104);
-x_107 = l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__11(x_3, x_106, x_104, x_103);
-lean::dec(x_106);
-lean::dec(x_3);
-x_110 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_110, 0, x_107);
-lean::cnstr_set(x_110, 1, x_1);
-return x_110;
-}
-case 10:
-{
-obj* x_114; obj* x_115; obj* x_117; obj* x_118; obj* x_121; 
-lean::dec(x_4);
-lean::dec(x_8);
-lean::dec(x_2);
-x_114 = lean::array_push(x_7, x_6);
-x_115 = lean::mk_nat_obj(0ul);
-lean::inc(x_3);
-x_117 = l_Array_reverseAux___main___rarg(x_3, x_115);
-x_118 = l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__12(x_3, x_117, x_115, x_114);
-lean::dec(x_117);
-lean::dec(x_3);
-x_121 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_121, 0, x_118);
-lean::cnstr_set(x_121, 1, x_1);
-return x_121;
-}
-case 11:
-{
-obj* x_125; obj* x_126; obj* x_128; obj* x_129; obj* x_132; 
-lean::dec(x_4);
-lean::dec(x_8);
-lean::dec(x_2);
-x_125 = lean::array_push(x_7, x_6);
-x_126 = lean::mk_nat_obj(0ul);
-lean::inc(x_3);
-x_128 = l_Array_reverseAux___main___rarg(x_3, x_126);
-x_129 = l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__13(x_3, x_128, x_126, x_125);
-lean::dec(x_128);
-lean::dec(x_3);
-x_132 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_132, 0, x_129);
-lean::cnstr_set(x_132, 1, x_1);
-return x_132;
-}
-case 12:
-{
-obj* x_136; obj* x_137; obj* x_139; obj* x_140; obj* x_143; 
-lean::dec(x_4);
-lean::dec(x_8);
-lean::dec(x_2);
-x_136 = lean::array_push(x_7, x_6);
-x_137 = lean::mk_nat_obj(0ul);
-lean::inc(x_3);
-x_139 = l_Array_reverseAux___main___rarg(x_3, x_137);
-x_140 = l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__14(x_3, x_139, x_137, x_136);
-lean::dec(x_139);
-lean::dec(x_3);
-x_143 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_143, 0, x_140);
-lean::cnstr_set(x_143, 1, x_1);
-return x_143;
-}
-case 13:
-{
-obj* x_147; obj* x_148; obj* x_150; obj* x_151; obj* x_154; 
-lean::dec(x_4);
-lean::dec(x_8);
-lean::dec(x_2);
-x_147 = lean::array_push(x_7, x_6);
-x_148 = lean::mk_nat_obj(0ul);
-lean::inc(x_3);
-x_150 = l_Array_reverseAux___main___rarg(x_3, x_148);
-x_151 = l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__15(x_3, x_150, x_148, x_147);
-lean::dec(x_150);
-lean::dec(x_3);
-x_154 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_154, 0, x_151);
-lean::cnstr_set(x_154, 1, x_1);
-return x_154;
-}
-default:
-{
-obj* x_157; obj* x_158; 
-lean::dec(x_8);
-lean::inc(x_6);
-x_157 = lean::array_push(x_3, x_6);
-x_158 = l_Lean_IR_FnBody_collectFreeVars(x_6, x_4);
-x_0 = x_7;
-x_3 = x_157;
-x_4 = x_158;
-goto _start;
-}
-}
-}
-case 1:
-{
-obj* x_162; obj* x_163; obj* x_165; obj* x_166; obj* x_169; 
-lean::dec(x_4);
-lean::dec(x_2);
-x_162 = lean::array_push(x_7, x_6);
-x_163 = lean::mk_nat_obj(0ul);
-lean::inc(x_3);
-x_165 = l_Array_reverseAux___main___rarg(x_3, x_163);
-x_166 = l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__16(x_3, x_165, x_163, x_162);
-lean::dec(x_165);
-lean::dec(x_3);
-x_169 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_169, 0, x_166);
-lean::cnstr_set(x_169, 1, x_1);
-return x_169;
-}
-case 2:
-{
-obj* x_172; obj* x_173; obj* x_175; obj* x_176; obj* x_179; 
-lean::dec(x_4);
-lean::dec(x_2);
-x_172 = lean::array_push(x_7, x_6);
-x_173 = lean::mk_nat_obj(0ul);
-lean::inc(x_3);
-x_175 = l_Array_reverseAux___main___rarg(x_3, x_173);
-x_176 = l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__17(x_3, x_175, x_173, x_172);
-lean::dec(x_175);
-lean::dec(x_3);
-x_179 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_179, 0, x_176);
-lean::cnstr_set(x_179, 1, x_1);
-return x_179;
-}
-case 3:
-{
-obj* x_182; obj* x_183; obj* x_185; obj* x_186; obj* x_189; 
-lean::dec(x_4);
-lean::dec(x_2);
-x_182 = lean::array_push(x_7, x_6);
-x_183 = lean::mk_nat_obj(0ul);
-lean::inc(x_3);
-x_185 = l_Array_reverseAux___main___rarg(x_3, x_183);
-x_186 = l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__18(x_3, x_185, x_183, x_182);
-lean::dec(x_185);
-lean::dec(x_3);
-x_189 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_189, 0, x_186);
-lean::cnstr_set(x_189, 1, x_1);
-return x_189;
-}
 case 4:
 {
-obj* x_192; obj* x_193; obj* x_195; obj* x_196; obj* x_199; 
-lean::dec(x_4);
-lean::dec(x_2);
-x_192 = lean::array_push(x_7, x_6);
-x_193 = lean::mk_nat_obj(0ul);
-lean::inc(x_3);
-x_195 = l_Array_reverseAux___main___rarg(x_3, x_193);
-x_196 = l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__19(x_3, x_195, x_193, x_192);
-lean::dec(x_195);
-lean::dec(x_3);
-x_199 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_199, 0, x_196);
-lean::cnstr_set(x_199, 1, x_1);
-return x_199;
+obj* x_36; obj* x_37; 
+lean::dec(x_8);
+lean::inc(x_6);
+x_36 = lean::array_push(x_3, x_6);
+x_37 = l_Lean_IR_FnBody_collectFreeVars(x_6, x_4);
+x_0 = x_7;
+x_3 = x_36;
+x_4 = x_37;
+goto _start;
 }
 case 5:
 {
-obj* x_202; obj* x_203; obj* x_205; obj* x_206; obj* x_209; 
-lean::dec(x_4);
-lean::dec(x_2);
-x_202 = lean::array_push(x_7, x_6);
-x_203 = lean::mk_nat_obj(0ul);
-lean::inc(x_3);
-x_205 = l_Array_reverseAux___main___rarg(x_3, x_203);
-x_206 = l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__20(x_3, x_205, x_203, x_202);
-lean::dec(x_205);
-lean::dec(x_3);
-x_209 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_209, 0, x_206);
-lean::cnstr_set(x_209, 1, x_1);
-return x_209;
-}
-case 6:
-{
-obj* x_212; obj* x_213; obj* x_215; obj* x_216; obj* x_219; 
-lean::dec(x_4);
-lean::dec(x_2);
-x_212 = lean::array_push(x_7, x_6);
-x_213 = lean::mk_nat_obj(0ul);
-lean::inc(x_3);
-x_215 = l_Array_reverseAux___main___rarg(x_3, x_213);
-x_216 = l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__21(x_3, x_215, x_213, x_212);
-lean::dec(x_215);
-lean::dec(x_3);
-x_219 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_219, 0, x_216);
-lean::cnstr_set(x_219, 1, x_1);
-return x_219;
-}
-case 7:
-{
-obj* x_222; obj* x_223; obj* x_225; obj* x_226; obj* x_229; 
-lean::dec(x_4);
-lean::dec(x_2);
-x_222 = lean::array_push(x_7, x_6);
-x_223 = lean::mk_nat_obj(0ul);
-lean::inc(x_3);
-x_225 = l_Array_reverseAux___main___rarg(x_3, x_223);
-x_226 = l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__22(x_3, x_225, x_223, x_222);
-lean::dec(x_225);
-lean::dec(x_3);
-x_229 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_229, 0, x_226);
-lean::cnstr_set(x_229, 1, x_1);
-return x_229;
-}
-case 8:
-{
-obj* x_232; obj* x_233; obj* x_235; obj* x_236; obj* x_239; 
-lean::dec(x_4);
-lean::dec(x_2);
-x_232 = lean::array_push(x_7, x_6);
-x_233 = lean::mk_nat_obj(0ul);
-lean::inc(x_3);
-x_235 = l_Array_reverseAux___main___rarg(x_3, x_233);
-x_236 = l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__23(x_3, x_235, x_233, x_232);
-lean::dec(x_235);
-lean::dec(x_3);
-x_239 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_239, 0, x_236);
-lean::cnstr_set(x_239, 1, x_1);
-return x_239;
-}
-case 9:
-{
-obj* x_242; obj* x_243; obj* x_245; obj* x_246; obj* x_249; 
-lean::dec(x_4);
-lean::dec(x_2);
-x_242 = lean::array_push(x_7, x_6);
-x_243 = lean::mk_nat_obj(0ul);
-lean::inc(x_3);
-x_245 = l_Array_reverseAux___main___rarg(x_3, x_243);
-x_246 = l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__24(x_3, x_245, x_243, x_242);
-lean::dec(x_245);
-lean::dec(x_3);
-x_249 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_249, 0, x_246);
-lean::cnstr_set(x_249, 1, x_1);
-return x_249;
-}
-case 10:
-{
-obj* x_252; obj* x_253; obj* x_255; obj* x_256; obj* x_259; 
-lean::dec(x_4);
-lean::dec(x_2);
-x_252 = lean::array_push(x_7, x_6);
-x_253 = lean::mk_nat_obj(0ul);
-lean::inc(x_3);
-x_255 = l_Array_reverseAux___main___rarg(x_3, x_253);
-x_256 = l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__25(x_3, x_255, x_253, x_252);
-lean::dec(x_255);
-lean::dec(x_3);
-x_259 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_259, 0, x_256);
-lean::cnstr_set(x_259, 1, x_1);
-return x_259;
-}
-case 11:
-{
-obj* x_262; obj* x_263; obj* x_265; obj* x_266; obj* x_269; 
-lean::dec(x_4);
-lean::dec(x_2);
-x_262 = lean::array_push(x_7, x_6);
-x_263 = lean::mk_nat_obj(0ul);
-lean::inc(x_3);
-x_265 = l_Array_reverseAux___main___rarg(x_3, x_263);
-x_266 = l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__26(x_3, x_265, x_263, x_262);
-lean::dec(x_265);
-lean::dec(x_3);
-x_269 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_269, 0, x_266);
-lean::cnstr_set(x_269, 1, x_1);
-return x_269;
+obj* x_41; obj* x_42; 
+lean::dec(x_8);
+lean::inc(x_6);
+x_41 = lean::array_push(x_3, x_6);
+x_42 = l_Lean_IR_FnBody_collectFreeVars(x_6, x_4);
+x_0 = x_7;
+x_3 = x_41;
+x_4 = x_42;
+goto _start;
 }
 default:
 {
-obj* x_272; obj* x_273; obj* x_275; obj* x_276; obj* x_279; 
+obj* x_47; obj* x_48; obj* x_49; obj* x_50; obj* x_52; 
+lean::dec(x_4);
+lean::dec(x_8);
+lean::dec(x_2);
+x_47 = lean::array_push(x_7, x_6);
+x_48 = lean::mk_nat_obj(0ul);
+x_49 = l_Array_reverseAux___main___rarg(x_3, x_48);
+x_50 = l_Array_miterateAux___main___at_Array_append___spec__1___rarg(x_49, x_49, x_48, x_47);
+lean::dec(x_49);
+x_52 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_52, 0, x_50);
+lean::cnstr_set(x_52, 1, x_1);
+return x_52;
+}
+}
+}
+default:
+{
+obj* x_55; obj* x_56; obj* x_57; obj* x_58; obj* x_60; 
 lean::dec(x_4);
 lean::dec(x_2);
-x_272 = lean::array_push(x_7, x_6);
-x_273 = lean::mk_nat_obj(0ul);
-lean::inc(x_3);
-x_275 = l_Array_reverseAux___main___rarg(x_3, x_273);
-x_276 = l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__27(x_3, x_275, x_273, x_272);
-lean::dec(x_275);
-lean::dec(x_3);
-x_279 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_279, 0, x_276);
-lean::cnstr_set(x_279, 1, x_1);
-return x_279;
+x_55 = lean::array_push(x_7, x_6);
+x_56 = lean::mk_nat_obj(0ul);
+x_57 = l_Array_reverseAux___main___rarg(x_3, x_56);
+x_58 = l_Array_miterateAux___main___at_Array_append___spec__1___rarg(x_57, x_57, x_56, x_55);
+lean::dec(x_57);
+x_60 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_60, 0, x_58);
+lean::cnstr_set(x_60, 1, x_1);
+return x_60;
 }
 }
 }
 else
 {
-obj* x_283; obj* x_284; obj* x_285; 
+obj* x_64; obj* x_65; obj* x_66; 
 lean::dec(x_4);
 lean::dec(x_0);
 lean::dec(x_2);
-x_283 = lean::mk_nat_obj(0ul);
-x_284 = l_Array_reverseAux___main___rarg(x_3, x_283);
-x_285 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_285, 0, x_284);
-lean::cnstr_set(x_285, 1, x_1);
-return x_285;
+x_64 = lean::mk_nat_obj(0ul);
+x_65 = l_Array_reverseAux___main___rarg(x_3, x_64);
+x_66 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_66, 0, x_65);
+lean::cnstr_set(x_66, 1, x_1);
+return x_66;
 }
 }
 }
@@ -1459,41 +457,11 @@ lean::dec(x_0);
 return x_1;
 }
 }
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__2___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; 
-x_4 = l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__2(x_0, x_1, x_2, x_3);
-lean::dec(x_0);
-lean::dec(x_1);
-return x_4;
-}
-}
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__3___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; 
-x_4 = l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__3(x_0, x_1, x_2, x_3);
-lean::dec(x_0);
-lean::dec(x_1);
-return x_4;
-}
-}
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__4___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; 
-x_4 = l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__4(x_0, x_1, x_2, x_3);
-lean::dec(x_0);
-lean::dec(x_1);
-return x_4;
-}
-}
-obj* l_Array_anyAux___main___at_Lean_IR_pushProjs___main___spec__5___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
+obj* l_Array_anyAux___main___at_Lean_IR_pushProjs___main___spec__2___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
 _start:
 {
 uint8 x_4; obj* x_5; 
-x_4 = l_Array_anyAux___main___at_Lean_IR_pushProjs___main___spec__5(x_0, x_1, x_2, x_3);
+x_4 = l_Array_anyAux___main___at_Lean_IR_pushProjs___main___spec__2(x_0, x_1, x_2, x_3);
 x_5 = lean::box(x_4);
 lean::dec(x_0);
 lean::dec(x_1);
@@ -1501,227 +469,27 @@ lean::dec(x_2);
 return x_5;
 }
 }
-obj* l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__6___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
+obj* l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__3___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
 _start:
 {
 obj* x_6; 
-x_6 = l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__6(x_0, x_1, x_2, x_3, x_4, x_5);
+x_6 = l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__3(x_0, x_1, x_2, x_3, x_4, x_5);
 lean::dec(x_0);
 lean::dec(x_2);
 lean::dec(x_3);
 return x_6;
 }
 }
-obj* l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__7___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
+obj* l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__4___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
 _start:
 {
 obj* x_5; 
-x_5 = l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__7(x_0, x_1, x_2, x_3, x_4);
+x_5 = l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__4(x_0, x_1, x_2, x_3, x_4);
 lean::dec(x_1);
 lean::dec(x_2);
 return x_5;
 }
 }
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__8___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; 
-x_4 = l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__8(x_0, x_1, x_2, x_3);
-lean::dec(x_0);
-lean::dec(x_1);
-return x_4;
-}
-}
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__9___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; 
-x_4 = l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__9(x_0, x_1, x_2, x_3);
-lean::dec(x_0);
-lean::dec(x_1);
-return x_4;
-}
-}
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__10___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; 
-x_4 = l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__10(x_0, x_1, x_2, x_3);
-lean::dec(x_0);
-lean::dec(x_1);
-return x_4;
-}
-}
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__11___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; 
-x_4 = l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__11(x_0, x_1, x_2, x_3);
-lean::dec(x_0);
-lean::dec(x_1);
-return x_4;
-}
-}
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__12___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; 
-x_4 = l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__12(x_0, x_1, x_2, x_3);
-lean::dec(x_0);
-lean::dec(x_1);
-return x_4;
-}
-}
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__13___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; 
-x_4 = l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__13(x_0, x_1, x_2, x_3);
-lean::dec(x_0);
-lean::dec(x_1);
-return x_4;
-}
-}
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__14___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; 
-x_4 = l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__14(x_0, x_1, x_2, x_3);
-lean::dec(x_0);
-lean::dec(x_1);
-return x_4;
-}
-}
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__15___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; 
-x_4 = l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__15(x_0, x_1, x_2, x_3);
-lean::dec(x_0);
-lean::dec(x_1);
-return x_4;
-}
-}
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__16___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; 
-x_4 = l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__16(x_0, x_1, x_2, x_3);
-lean::dec(x_0);
-lean::dec(x_1);
-return x_4;
-}
-}
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__17___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; 
-x_4 = l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__17(x_0, x_1, x_2, x_3);
-lean::dec(x_0);
-lean::dec(x_1);
-return x_4;
-}
-}
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__18___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; 
-x_4 = l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__18(x_0, x_1, x_2, x_3);
-lean::dec(x_0);
-lean::dec(x_1);
-return x_4;
-}
-}
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__19___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; 
-x_4 = l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__19(x_0, x_1, x_2, x_3);
-lean::dec(x_0);
-lean::dec(x_1);
-return x_4;
-}
-}
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__20___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; 
-x_4 = l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__20(x_0, x_1, x_2, x_3);
-lean::dec(x_0);
-lean::dec(x_1);
-return x_4;
-}
-}
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__21___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; 
-x_4 = l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__21(x_0, x_1, x_2, x_3);
-lean::dec(x_0);
-lean::dec(x_1);
-return x_4;
-}
-}
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__22___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; 
-x_4 = l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__22(x_0, x_1, x_2, x_3);
-lean::dec(x_0);
-lean::dec(x_1);
-return x_4;
-}
-}
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__23___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; 
-x_4 = l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__23(x_0, x_1, x_2, x_3);
-lean::dec(x_0);
-lean::dec(x_1);
-return x_4;
-}
-}
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__24___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; 
-x_4 = l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__24(x_0, x_1, x_2, x_3);
-lean::dec(x_0);
-lean::dec(x_1);
-return x_4;
-}
-}
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__25___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; 
-x_4 = l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__25(x_0, x_1, x_2, x_3);
-lean::dec(x_0);
-lean::dec(x_1);
-return x_4;
-}
-}
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__26___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; 
-x_4 = l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__26(x_0, x_1, x_2, x_3);
-lean::dec(x_0);
-lean::dec(x_1);
-return x_4;
-}
-}
-obj* l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__27___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; 
-x_4 = l_Array_miterateAux___main___at_Lean_IR_pushProjs___main___spec__27(x_0, x_1, x_2, x_3);
-lean::dec(x_0);
-lean::dec(x_1);
-return x_4;
-}
-}
 obj* l_Lean_IR_pushProjs(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
 _start:
 {
@@ -1775,7 +543,7 @@ else
 {
 obj* x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_10; 
 x_6 = lean::array_index(x_1, x_0);
-x_7 = l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__6___closed__1;
+x_7 = l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__3___closed__1;
 x_8 = lean::array_update(x_1, x_0, x_7);
 x_9 = lean::mk_nat_obj(1ul);
 x_10 = lean::nat_add(x_0, x_9);
@@ -1974,8 +742,8 @@ 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_pushProjs___main___spec__6___closed__1 = _init_l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__6___closed__1();
-lean::mark_persistent(l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__6___closed__1);
+ l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__3___closed__1 = _init_l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__3___closed__1();
+lean::mark_persistent(l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__3___closed__1);
  l_Lean_IR_pushProjs___main___closed__1 = _init_l_Lean_IR_pushProjs___main___closed__1();
 lean::mark_persistent(l_Lean_IR_pushProjs___main___closed__1);
 return w;