diff --git a/stage0/src/library/constructions/CMakeLists.txt b/stage0/src/library/constructions/CMakeLists.txt
index d0470e0959..b115cc0a33 100644
--- a/stage0/src/library/constructions/CMakeLists.txt
+++ b/stage0/src/library/constructions/CMakeLists.txt
@@ -1,3 +1,3 @@
-add_library(constructions OBJECT rec_on.cpp cases_on.cpp
+add_library(constructions OBJECT cases_on.cpp
   no_confusion.cpp projection.cpp brec_on.cpp init_module.cpp
   util.cpp)
diff --git a/stage0/src/library/constructions/rec_on.cpp b/stage0/src/library/constructions/rec_on.cpp
deleted file mode 100644
index 4af570505e..0000000000
--- a/stage0/src/library/constructions/rec_on.cpp
+++ /dev/null
@@ -1,64 +0,0 @@
-/*
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include "runtime/sstream.h"
-#include "kernel/kernel_exception.h"
-#include "kernel/environment.h"
-#include "kernel/instantiate.h"
-#include "kernel/abstract.h"
-#include "kernel/inductive.h"
-#include "library/reducible.h"
-#include "library/suffixes.h"
-#include "library/aux_recursors.h"
-#include "library/constructions/util.h"
-
-namespace lean {
-declaration mk_rec_on(environment const & env, name const & n) {
-    constant_info ind_info = env.get(n);
-    if (!ind_info.is_inductive())
-        throw exception(sstream() << "error in '" << g_rec_on << "' generation, '" << n << "' is not an inductive datatype");
-    name_generator ngen = mk_constructions_name_generator();
-    local_ctx lctx;
-    name rec_on_name(n, g_rec_on);
-    constant_info rec_info = env.get(mk_rec_name(n));
-    recursor_val  rec_val  = rec_info.to_recursor_val();
-    buffer<expr> locals;
-    expr rec_type = rec_info.get_type();
-    while (is_pi(rec_type)) {
-        expr local = lctx.mk_local_decl(ngen, binding_name(rec_type), binding_domain(rec_type), binding_info(rec_type));
-        rec_type   = instantiate(binding_body(rec_type), local);
-        locals.push_back(local);
-    }
-
-    // locals order
-    //   As Cs minor_premises indices major-premise
-
-    // new_locals order
-    //   As Cs indices major-premise minor-premises
-    buffer<expr> new_locals;
-    unsigned num_indices  = rec_val.get_nindices();
-    unsigned num_minors   = rec_val.get_nminors();
-    unsigned AC_sz        = locals.size() - num_minors - num_indices - 1;
-    for (unsigned i = 0; i < AC_sz; i++)
-        new_locals.push_back(locals[i]);
-    for (unsigned i = 0; i < num_indices + 1; i++)
-        new_locals.push_back(locals[AC_sz + num_minors + i]);
-    for (unsigned i = 0; i < num_minors; i++)
-        new_locals.push_back(locals[AC_sz + i]);
-    expr rec_on_type = lctx.mk_pi(new_locals, rec_type);
-
-    levels ls = lparams_to_levels(rec_info.get_lparams());
-    expr rec  = mk_constant(rec_info.get_name(), ls);
-    expr rec_on_val = lctx.mk_lambda(new_locals, mk_app(rec, locals));
-
-    return mk_definition_inferring_unsafe(env, rec_on_name, rec_info.get_lparams(),
-                                          rec_on_type, rec_on_val, reducibility_hints::mk_abbreviation());
-}
-
-extern "C" LEAN_EXPORT object * lean_mk_rec_on(object * env, object * n) {
-    return catch_kernel_exceptions<declaration>([&]() { return mk_rec_on(environment(env), name(n, true)); });
-}
-}
diff --git a/stage0/src/library/constructions/rec_on.h b/stage0/src/library/constructions/rec_on.h
deleted file mode 100644
index cf2b6107d5..0000000000
--- a/stage0/src/library/constructions/rec_on.h
+++ /dev/null
@@ -1,19 +0,0 @@
-/*
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "kernel/environment.h"
-
-namespace lean {
-/** \brief Given an inductive datatype \c n in \c env, returns
-    the declaration for <tt>n.rec_on</tt>.
-
-    \remark <tt>rec_on</tt> is based on <tt>n.rec</tt>
-
-    \remark Throws an exception if \c n is not an inductive datatype.
-*/
-declaration mk_rec_on(environment const & env, name const & n);
-}
diff --git a/stage0/src/library/suffixes.h b/stage0/src/library/suffixes.h
index 06144335fc..3d39166092 100644
--- a/stage0/src/library/suffixes.h
+++ b/stage0/src/library/suffixes.h
@@ -8,7 +8,6 @@ Author: Leonardo de Moura
 
 namespace lean {
 constexpr char const * g_rec               = "rec";
-constexpr char const * g_rec_on            = "recOn";
 constexpr char const * g_brec_on           = "brecOn";
 constexpr char const * g_binduction_on     = "binductionOn";
 constexpr char const * g_cases_on          = "casesOn";
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index 658ab0874e..0699845ba4 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -8,7 +8,7 @@ options get_default_options() {
     // switch to `true` for ABI-breaking changes affecting meta code
     opts = opts.update({"interpreter", "prefer_native"}, false);
     // switch to `true` for changing built-in parsers used in quotations
-    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, true);
+    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false);
     // toggling `parseQuotWithCurrentStage` may also require toggling the following option if macros/syntax
     // with custom precheck hooks were affected
     opts = opts.update({"quotPrecheck"}, true);
diff --git a/stage0/src/util/ffi.cpp b/stage0/src/util/ffi.cpp
index 923fe818c3..6e53d7cca5 100644
--- a/stage0/src/util/ffi.cpp
+++ b/stage0/src/util/ffi.cpp
@@ -13,7 +13,15 @@ extern "C" object * lean_get_leanc_extra_flags(object *) {
     return lean_mk_string("@LEANC_EXTRA_FLAGS@");
 }
 
+extern "C" object * lean_get_leanc_internal_flags(object *) {
+    return lean_mk_string("@LEANC_INTERNAL_FLAGS@");
+}
+
 extern "C" object * lean_get_linker_flags(uint8 link_static) {
     return lean_mk_string(link_static ? "@LEANC_STATIC_LINKER_FLAGS@ @LEAN_EXTRA_LINKER_FLAGS@" : "@LEANC_SHARED_LINKER_FLAGS@ @LEAN_EXTRA_LINKER_FLAGS@");
 }
+
+extern "C" object * lean_get_internal_linker_flags(object *) {
+    return lean_mk_string("@LEANC_INTERNAL_LINKER_FLAGS@");
+}
 }
diff --git a/stage0/stdlib/Init/Tactics.c b/stage0/stdlib/Init/Tactics.c
index 687102ae7a..27155a685d 100644
--- a/stage0/stdlib/Init/Tactics.c
+++ b/stage0/stdlib/Init/Tactics.c
@@ -6410,7 +6410,7 @@ static lean_object* _init_l_Lean_Parser_Tactic___aux__Init__Tactics______macroRu
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string_unchecked("\"The rfl tactic failed. Possible reasons:\n- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).\n- The arguments of the relation are not equal.\nTry using the reflexivitiy lemma for your relation explicitly, e.g. `exact Eq.rfl`.\"", 263, 263);
+x_1 = lean_mk_string_unchecked("\"The rfl tactic failed. Possible reasons:\n- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).\n- The arguments of the relation are not equal.\nTry using the reflexivity lemma for your relation explicitly, e.g. `exact Eq.refl _` or\n`exact HEq.rfl` etc.\"", 288, 288);
 return x_1;
 }
 }
diff --git a/stage0/stdlib/Lake/Build/Module.c b/stage0/stdlib/Lake/Build/Module.c
index e344c536ac..daa02d34de 100644
--- a/stage0/stdlib/Lake/Build/Module.c
+++ b/stage0/stdlib/Lake/Build/Module.c
@@ -173,7 +173,7 @@ LEAN_EXPORT lean_object* l_Lake_Module_cacheOutputHashes(lean_object*, lean_obje
 LEAN_EXPORT lean_object* l_Lake_Module_dynlibFacetConfig;
 LEAN_EXPORT lean_object* l_Lean_HashSetImp_contains___at_Lake_Module_recBuildDeps___spec__4___boxed(lean_object*, lean_object*);
 static lean_object* l_Lake_Module_recBuildLeanBcToO___lambda__1___closed__1;
-LEAN_EXPORT lean_object* l_Lake_Module_recBuildDeps___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, size_t, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Lake_Module_recBuildDeps___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, size_t, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lake_initModuleFacetConfigs___closed__12;
 lean_object* l_Lake_Workspace_findModule_x3f___boxed(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lake_Module_recBuildDynlib___lambda__4(lean_object*, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -13121,48 +13121,48 @@ lean_ctor_set(x_3, 1, x_1);
 return x_3;
 }
 }
-LEAN_EXPORT lean_object* l_Lake_Module_recBuildDeps___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, size_t x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
+LEAN_EXPORT lean_object* l_Lake_Module_recBuildDeps___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, size_t x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
 _start:
 {
 uint8_t x_10; 
 x_10 = !lean_is_exclusive(x_9);
 if (x_10 == 0)
 {
-lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; size_t x_23; lean_object* x_24; lean_object* x_25; size_t x_26; lean_object* x_27; lean_object* x_28; 
+lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; size_t x_22; lean_object* x_23; lean_object* x_24; size_t x_25; lean_object* x_26; lean_object* x_27; 
 x_11 = lean_ctor_get(x_9, 0);
 x_12 = lean_ctor_get(x_9, 1);
 x_13 = l_Lake_BuildTrace_mix(x_1, x_2);
-x_14 = l_Lake_BuildTrace_mix(x_3, x_13);
-x_15 = lean_ctor_get(x_4, 1);
-x_16 = lean_ctor_get(x_15, 0);
-x_17 = lean_ctor_get(x_16, 8);
-x_18 = lean_array_get_size(x_11);
-x_19 = lean_unsigned_to_nat(0u);
-x_20 = l_Array_filterMapM___at_Lake_Module_recBuildDeps___spec__12(x_11, x_19, x_18);
-x_21 = l_Array_append___rarg(x_5, x_20);
-lean_dec(x_20);
-x_22 = lean_array_to_list(lean_box(0), x_21);
-x_23 = lean_usize_of_nat(x_18);
-lean_dec(x_18);
-x_24 = l_Array_mapMUnsafe_map___at_Lake_Module_recBuildDeps___spec__14(x_23, x_6, x_11);
-x_25 = lean_array_get_size(x_7);
-x_26 = lean_usize_of_nat(x_25);
-lean_dec(x_25);
-x_27 = l_Array_mapMUnsafe_map___at_Lake_Module_recBuildDeps___spec__14(x_26, x_6, x_7);
-x_28 = l_Array_append___rarg(x_24, x_27);
-lean_dec(x_27);
-lean_ctor_set(x_9, 1, x_28);
-lean_ctor_set(x_9, 0, x_22);
-if (lean_obj_tag(x_17) == 0)
+x_14 = lean_ctor_get(x_3, 1);
+x_15 = lean_ctor_get(x_14, 0);
+x_16 = lean_ctor_get(x_15, 8);
+x_17 = lean_array_get_size(x_11);
+x_18 = lean_unsigned_to_nat(0u);
+x_19 = l_Array_filterMapM___at_Lake_Module_recBuildDeps___spec__12(x_11, x_18, x_17);
+x_20 = l_Array_append___rarg(x_4, x_19);
+lean_dec(x_19);
+x_21 = lean_array_to_list(lean_box(0), x_20);
+x_22 = lean_usize_of_nat(x_17);
+lean_dec(x_17);
+x_23 = l_Array_mapMUnsafe_map___at_Lake_Module_recBuildDeps___spec__14(x_22, x_5, x_11);
+x_24 = lean_array_get_size(x_6);
+x_25 = lean_usize_of_nat(x_24);
+lean_dec(x_24);
+x_26 = l_Array_mapMUnsafe_map___at_Lake_Module_recBuildDeps___spec__14(x_25, x_5, x_6);
+x_27 = l_Array_append___rarg(x_23, x_26);
+lean_dec(x_26);
+lean_ctor_set(x_9, 1, x_27);
+lean_ctor_set(x_9, 0, x_21);
+if (lean_obj_tag(x_16) == 0)
 {
-lean_object* x_29; lean_object* x_30; lean_object* x_31; 
-x_29 = lean_ctor_get(x_8, 2);
-x_30 = lean_ctor_get(x_29, 1);
-x_31 = lean_ctor_get(x_30, 8);
-if (lean_obj_tag(x_31) == 0)
+lean_object* x_28; lean_object* x_29; lean_object* x_30; 
+x_28 = lean_ctor_get(x_7, 2);
+x_29 = lean_ctor_get(x_28, 1);
+x_30 = lean_ctor_get(x_29, 8);
+if (lean_obj_tag(x_30) == 0)
 {
-lean_object* x_32; lean_object* x_33; 
-x_32 = l_Lake_BuildTrace_mix(x_14, x_12);
+lean_object* x_31; lean_object* x_32; lean_object* x_33; 
+x_31 = l_Lake_BuildTrace_mix(x_8, x_12);
+x_32 = l_Lake_BuildTrace_mix(x_13, x_31);
 x_33 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_33, 0, x_9);
 lean_ctor_set(x_33, 1, x_32);
@@ -13171,154 +13171,162 @@ return x_33;
 else
 {
 lean_object* x_34; uint8_t x_35; 
-x_34 = lean_ctor_get(x_31, 0);
+x_34 = lean_ctor_get(x_30, 0);
 x_35 = lean_unbox(x_34);
 if (x_35 == 0)
 {
-lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; 
+lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; 
 x_36 = l_Lake_Module_recBuildDeps___lambda__1___closed__3;
 x_37 = l_Lake_BuildTrace_mix(x_12, x_36);
-x_38 = l_Lake_BuildTrace_mix(x_14, x_37);
-x_39 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_39, 0, x_9);
-lean_ctor_set(x_39, 1, x_38);
-return x_39;
-}
-else
-{
-lean_object* x_40; 
-lean_dec(x_12);
+x_38 = l_Lake_BuildTrace_mix(x_8, x_37);
+x_39 = l_Lake_BuildTrace_mix(x_13, x_38);
 x_40 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_40, 0, x_9);
-lean_ctor_set(x_40, 1, x_14);
+lean_ctor_set(x_40, 1, x_39);
 return x_40;
 }
-}
-}
 else
 {
-lean_object* x_41; uint8_t x_42; 
-x_41 = lean_ctor_get(x_17, 0);
-x_42 = lean_unbox(x_41);
-if (x_42 == 0)
-{
-lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; 
-x_43 = l_Lake_Module_recBuildDeps___lambda__1___closed__3;
-x_44 = l_Lake_BuildTrace_mix(x_12, x_43);
-x_45 = l_Lake_BuildTrace_mix(x_14, x_44);
-x_46 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_46, 0, x_9);
-lean_ctor_set(x_46, 1, x_45);
-return x_46;
-}
-else
-{
-lean_object* x_47; 
+lean_object* x_41; 
 lean_dec(x_12);
-x_47 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_47, 0, x_9);
-lean_ctor_set(x_47, 1, x_14);
-return x_47;
+lean_dec(x_8);
+x_41 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_41, 0, x_9);
+lean_ctor_set(x_41, 1, x_13);
+return x_41;
 }
 }
 }
 else
 {
-lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; size_t x_60; lean_object* x_61; lean_object* x_62; size_t x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; 
-x_48 = lean_ctor_get(x_9, 0);
-x_49 = lean_ctor_get(x_9, 1);
-lean_inc(x_49);
-lean_inc(x_48);
+lean_object* x_42; uint8_t x_43; 
+x_42 = lean_ctor_get(x_16, 0);
+x_43 = lean_unbox(x_42);
+if (x_43 == 0)
+{
+lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; 
+x_44 = l_Lake_Module_recBuildDeps___lambda__1___closed__3;
+x_45 = l_Lake_BuildTrace_mix(x_12, x_44);
+x_46 = l_Lake_BuildTrace_mix(x_8, x_45);
+x_47 = l_Lake_BuildTrace_mix(x_13, x_46);
+x_48 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_48, 0, x_9);
+lean_ctor_set(x_48, 1, x_47);
+return x_48;
+}
+else
+{
+lean_object* x_49; 
+lean_dec(x_12);
+lean_dec(x_8);
+x_49 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_49, 0, x_9);
+lean_ctor_set(x_49, 1, x_13);
+return x_49;
+}
+}
+}
+else
+{
+lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; size_t x_61; lean_object* x_62; lean_object* x_63; size_t x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; 
+x_50 = lean_ctor_get(x_9, 0);
+x_51 = lean_ctor_get(x_9, 1);
+lean_inc(x_51);
+lean_inc(x_50);
 lean_dec(x_9);
-x_50 = l_Lake_BuildTrace_mix(x_1, x_2);
-x_51 = l_Lake_BuildTrace_mix(x_3, x_50);
-x_52 = lean_ctor_get(x_4, 1);
-x_53 = lean_ctor_get(x_52, 0);
-x_54 = lean_ctor_get(x_53, 8);
-x_55 = lean_array_get_size(x_48);
-x_56 = lean_unsigned_to_nat(0u);
-x_57 = l_Array_filterMapM___at_Lake_Module_recBuildDeps___spec__12(x_48, x_56, x_55);
-x_58 = l_Array_append___rarg(x_5, x_57);
-lean_dec(x_57);
-x_59 = lean_array_to_list(lean_box(0), x_58);
-x_60 = lean_usize_of_nat(x_55);
-lean_dec(x_55);
-x_61 = l_Array_mapMUnsafe_map___at_Lake_Module_recBuildDeps___spec__14(x_60, x_6, x_48);
-x_62 = lean_array_get_size(x_7);
-x_63 = lean_usize_of_nat(x_62);
-lean_dec(x_62);
-x_64 = l_Array_mapMUnsafe_map___at_Lake_Module_recBuildDeps___spec__14(x_63, x_6, x_7);
-x_65 = l_Array_append___rarg(x_61, x_64);
-lean_dec(x_64);
-x_66 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_66, 0, x_59);
-lean_ctor_set(x_66, 1, x_65);
-if (lean_obj_tag(x_54) == 0)
+x_52 = l_Lake_BuildTrace_mix(x_1, x_2);
+x_53 = lean_ctor_get(x_3, 1);
+x_54 = lean_ctor_get(x_53, 0);
+x_55 = lean_ctor_get(x_54, 8);
+x_56 = lean_array_get_size(x_50);
+x_57 = lean_unsigned_to_nat(0u);
+x_58 = l_Array_filterMapM___at_Lake_Module_recBuildDeps___spec__12(x_50, x_57, x_56);
+x_59 = l_Array_append___rarg(x_4, x_58);
+lean_dec(x_58);
+x_60 = lean_array_to_list(lean_box(0), x_59);
+x_61 = lean_usize_of_nat(x_56);
+lean_dec(x_56);
+x_62 = l_Array_mapMUnsafe_map___at_Lake_Module_recBuildDeps___spec__14(x_61, x_5, x_50);
+x_63 = lean_array_get_size(x_6);
+x_64 = lean_usize_of_nat(x_63);
+lean_dec(x_63);
+x_65 = l_Array_mapMUnsafe_map___at_Lake_Module_recBuildDeps___spec__14(x_64, x_5, x_6);
+x_66 = l_Array_append___rarg(x_62, x_65);
+lean_dec(x_65);
+x_67 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_67, 0, x_60);
+lean_ctor_set(x_67, 1, x_66);
+if (lean_obj_tag(x_55) == 0)
 {
-lean_object* x_67; lean_object* x_68; lean_object* x_69; 
-x_67 = lean_ctor_get(x_8, 2);
-x_68 = lean_ctor_get(x_67, 1);
-x_69 = lean_ctor_get(x_68, 8);
-if (lean_obj_tag(x_69) == 0)
+lean_object* x_68; lean_object* x_69; lean_object* x_70; 
+x_68 = lean_ctor_get(x_7, 2);
+x_69 = lean_ctor_get(x_68, 1);
+x_70 = lean_ctor_get(x_69, 8);
+if (lean_obj_tag(x_70) == 0)
 {
-lean_object* x_70; lean_object* x_71; 
-x_70 = l_Lake_BuildTrace_mix(x_51, x_49);
-x_71 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_71, 0, x_66);
-lean_ctor_set(x_71, 1, x_70);
-return x_71;
+lean_object* x_71; lean_object* x_72; lean_object* x_73; 
+x_71 = l_Lake_BuildTrace_mix(x_8, x_51);
+x_72 = l_Lake_BuildTrace_mix(x_52, x_71);
+x_73 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_73, 0, x_67);
+lean_ctor_set(x_73, 1, x_72);
+return x_73;
 }
 else
 {
-lean_object* x_72; uint8_t x_73; 
-x_72 = lean_ctor_get(x_69, 0);
-x_73 = lean_unbox(x_72);
-if (x_73 == 0)
+lean_object* x_74; uint8_t x_75; 
+x_74 = lean_ctor_get(x_70, 0);
+x_75 = lean_unbox(x_74);
+if (x_75 == 0)
 {
-lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77; 
-x_74 = l_Lake_Module_recBuildDeps___lambda__1___closed__3;
-x_75 = l_Lake_BuildTrace_mix(x_49, x_74);
-x_76 = l_Lake_BuildTrace_mix(x_51, x_75);
-x_77 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_77, 0, x_66);
-lean_ctor_set(x_77, 1, x_76);
-return x_77;
+lean_object* x_76; lean_object* x_77; lean_object* x_78; lean_object* x_79; lean_object* x_80; 
+x_76 = l_Lake_Module_recBuildDeps___lambda__1___closed__3;
+x_77 = l_Lake_BuildTrace_mix(x_51, x_76);
+x_78 = l_Lake_BuildTrace_mix(x_8, x_77);
+x_79 = l_Lake_BuildTrace_mix(x_52, x_78);
+x_80 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_80, 0, x_67);
+lean_ctor_set(x_80, 1, x_79);
+return x_80;
 }
 else
 {
-lean_object* x_78; 
-lean_dec(x_49);
-x_78 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_78, 0, x_66);
-lean_ctor_set(x_78, 1, x_51);
-return x_78;
+lean_object* x_81; 
+lean_dec(x_51);
+lean_dec(x_8);
+x_81 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_81, 0, x_67);
+lean_ctor_set(x_81, 1, x_52);
+return x_81;
 }
 }
 }
 else
 {
-lean_object* x_79; uint8_t x_80; 
-x_79 = lean_ctor_get(x_54, 0);
-x_80 = lean_unbox(x_79);
-if (x_80 == 0)
+lean_object* x_82; uint8_t x_83; 
+x_82 = lean_ctor_get(x_55, 0);
+x_83 = lean_unbox(x_82);
+if (x_83 == 0)
 {
-lean_object* x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84; 
-x_81 = l_Lake_Module_recBuildDeps___lambda__1___closed__3;
-x_82 = l_Lake_BuildTrace_mix(x_49, x_81);
-x_83 = l_Lake_BuildTrace_mix(x_51, x_82);
-x_84 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_84, 0, x_66);
-lean_ctor_set(x_84, 1, x_83);
-return x_84;
+lean_object* x_84; lean_object* x_85; lean_object* x_86; lean_object* x_87; lean_object* x_88; 
+x_84 = l_Lake_Module_recBuildDeps___lambda__1___closed__3;
+x_85 = l_Lake_BuildTrace_mix(x_51, x_84);
+x_86 = l_Lake_BuildTrace_mix(x_8, x_85);
+x_87 = l_Lake_BuildTrace_mix(x_52, x_86);
+x_88 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_88, 0, x_67);
+lean_ctor_set(x_88, 1, x_87);
+return x_88;
 }
 else
 {
-lean_object* x_85; 
-lean_dec(x_49);
-x_85 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_85, 0, x_66);
-lean_ctor_set(x_85, 1, x_51);
-return x_85;
+lean_object* x_89; 
+lean_dec(x_51);
+lean_dec(x_8);
+x_89 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_89, 0, x_67);
+lean_ctor_set(x_89, 1, x_52);
+return x_89;
 }
 }
 }
@@ -13419,13 +13427,13 @@ x_14 = lean_ctor_get(x_10, 1);
 x_15 = lean_box_usize(x_5);
 x_16 = lean_alloc_closure((void*)(l_Lake_Module_recBuildDeps___lambda__1___boxed), 9, 8);
 lean_closure_set(x_16, 0, x_1);
-lean_closure_set(x_16, 1, x_14);
-lean_closure_set(x_16, 2, x_2);
-lean_closure_set(x_16, 3, x_3);
-lean_closure_set(x_16, 4, x_4);
-lean_closure_set(x_16, 5, x_15);
-lean_closure_set(x_16, 6, x_13);
-lean_closure_set(x_16, 7, x_6);
+lean_closure_set(x_16, 1, x_2);
+lean_closure_set(x_16, 2, x_3);
+lean_closure_set(x_16, 3, x_4);
+lean_closure_set(x_16, 4, x_15);
+lean_closure_set(x_16, 5, x_13);
+lean_closure_set(x_16, 6, x_6);
+lean_closure_set(x_16, 7, x_14);
 x_17 = lean_alloc_closure((void*)(l_Lake_EResult_map___rarg), 2, 1);
 lean_closure_set(x_17, 0, x_16);
 x_18 = lean_ctor_get(x_7, 0);
@@ -13453,13 +13461,13 @@ lean_dec(x_10);
 x_27 = lean_box_usize(x_5);
 x_28 = lean_alloc_closure((void*)(l_Lake_Module_recBuildDeps___lambda__1___boxed), 9, 8);
 lean_closure_set(x_28, 0, x_1);
-lean_closure_set(x_28, 1, x_26);
-lean_closure_set(x_28, 2, x_2);
-lean_closure_set(x_28, 3, x_3);
-lean_closure_set(x_28, 4, x_4);
-lean_closure_set(x_28, 5, x_27);
-lean_closure_set(x_28, 6, x_25);
-lean_closure_set(x_28, 7, x_6);
+lean_closure_set(x_28, 1, x_2);
+lean_closure_set(x_28, 2, x_3);
+lean_closure_set(x_28, 3, x_4);
+lean_closure_set(x_28, 4, x_27);
+lean_closure_set(x_28, 5, x_25);
+lean_closure_set(x_28, 6, x_6);
+lean_closure_set(x_28, 7, x_26);
 x_29 = lean_alloc_closure((void*)(l_Lake_EResult_map___rarg), 2, 1);
 lean_closure_set(x_29, 0, x_28);
 x_30 = lean_ctor_get(x_7, 0);
@@ -13536,8 +13544,8 @@ lean_inc(x_13);
 lean_dec(x_1);
 x_14 = lean_box_usize(x_5);
 x_15 = lean_alloc_closure((void*)(l_Lake_Module_recBuildDeps___lambda__3___boxed), 9, 7);
-lean_closure_set(x_15, 0, x_12);
-lean_closure_set(x_15, 1, x_2);
+lean_closure_set(x_15, 0, x_2);
+lean_closure_set(x_15, 1, x_12);
 lean_closure_set(x_15, 2, x_3);
 lean_closure_set(x_15, 3, x_4);
 lean_closure_set(x_15, 4, x_14);
@@ -16080,11 +16088,11 @@ LEAN_EXPORT lean_object* l_Lake_Module_recBuildDeps___lambda__1___boxed(lean_obj
 _start:
 {
 size_t x_10; lean_object* x_11; 
-x_10 = lean_unbox_usize(x_6);
-lean_dec(x_6);
-x_11 = l_Lake_Module_recBuildDeps___lambda__1(x_1, x_2, x_3, x_4, x_5, x_10, x_7, x_8, x_9);
-lean_dec(x_8);
-lean_dec(x_4);
+x_10 = lean_unbox_usize(x_5);
+lean_dec(x_5);
+x_11 = l_Lake_Module_recBuildDeps___lambda__1(x_1, x_2, x_3, x_4, x_10, x_6, x_7, x_8, x_9);
+lean_dec(x_7);
+lean_dec(x_3);
 return x_11;
 }
 }
diff --git a/stage0/stdlib/Lean/Compiler/FFI.c b/stage0/stdlib/Lean/Compiler/FFI.c
index 1bf4cf75bf..a645039ee4 100644
--- a/stage0/stdlib/Lean/Compiler/FFI.c
+++ b/stage0/stdlib/Lean/Compiler/FFI.c
@@ -13,31 +13,69 @@
 #ifdef __cplusplus
 extern "C" {
 #endif
+static size_t l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__8;
 lean_object* lean_mk_empty_array_with_capacity(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_FFI_getLinkerFlags(lean_object*, uint8_t);
 LEAN_EXPORT lean_object* l_Lean_Compiler_FFI_getLinkerFlags___boxed(lean_object*, lean_object*);
 lean_object* l_System_FilePath_join(lean_object*, lean_object*);
 lean_object* lean_array_push(lean_object*, lean_object*);
 static lean_object* l_Lean_Compiler_FFI_getLinkerFlags___closed__2;
+static lean_object* l_Lean_Compiler_FFI_getInternalCFlags___closed__7;
 lean_object* l_String_trim(lean_object*);
 static lean_object* l_Lean_Compiler_FFI_getCFlags___closed__5;
+static lean_object* l_Lean_Compiler_FFI_getInternalCFlags___closed__1;
 static lean_object* l_Lean_Compiler_FFI_getLinkerFlags___closed__3;
 lean_object* lean_get_linker_flags(uint8_t);
 static lean_object* l_Lean_Compiler_FFI_getCFlags___closed__8;
 lean_object* lean_get_leanc_extra_flags(lean_object*);
+size_t lean_usize_of_nat(lean_object*);
+static lean_object* l_Lean_Compiler_FFI_getInternalCFlags___closed__5;
+static lean_object* l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__1;
+LEAN_EXPORT lean_object* l_Lean_Compiler_FFI_getInternalLinkerFlags___boxed(lean_object*);
+static size_t l_Lean_Compiler_FFI_getInternalCFlags___closed__8;
+static lean_object* l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__7;
+static lean_object* l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__6;
+static lean_object* l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__2;
+static lean_object* l_Array_mapMUnsafe_map___at_Lean_Compiler_FFI_getInternalCFlags___spec__1___closed__1;
 static lean_object* l_Lean_Compiler_FFI_getCFlags___closed__1;
+LEAN_EXPORT lean_object* l___private_Lean_Compiler_FFI_0__Lean_Compiler_FFI_getLeancInternalFlags___boxed(lean_object*);
 static lean_object* l_Lean_Compiler_FFI_getLinkerFlags___closed__1;
+static lean_object* l_Lean_Compiler_FFI_getInternalCFlags___closed__2;
+static lean_object* l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__5;
+LEAN_EXPORT lean_object* l___private_Lean_Compiler_FFI_0__Lean_Compiler_FFI_getBuiltinInternalLinkerFlags___boxed(lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Compiler_FFI_getInternalCFlags(lean_object*);
+LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Compiler_FFI_getInternalLinkerFlags___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l___private_Lean_Compiler_FFI_0__Lean_Compiler_FFI_getLeancExtraFlags___boxed(lean_object*);
+lean_object* l_String_replace(lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Compiler_FFI_getInternalLinkerFlags(lean_object*);
 LEAN_EXPORT lean_object* l___private_Lean_Compiler_FFI_0__Lean_Compiler_FFI_getBuiltinLinkerFlags___boxed(lean_object*);
+LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Compiler_FFI_getInternalLinkerFlags___spec__1(lean_object*, size_t, size_t, lean_object*);
+LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Compiler_FFI_getInternalCFlags___spec__1(lean_object*, size_t, size_t, lean_object*);
+lean_object* lean_get_internal_linker_flags(lean_object*);
+static lean_object* l_Lean_Compiler_FFI_getInternalCFlags___closed__4;
 static lean_object* l_Lean_Compiler_FFI_getCFlags___closed__7;
 static lean_object* l_Lean_Compiler_FFI_getCFlags___closed__2;
 lean_object* l_List_foldl___at_Array_appendList___spec__1___rarg(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_FFI_getCFlags(lean_object*);
 static lean_object* l_Lean_Compiler_FFI_getCFlags___closed__6;
+size_t lean_usize_add(size_t, size_t);
+lean_object* lean_array_uget(lean_object*, size_t);
+static lean_object* l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__3;
+LEAN_EXPORT lean_object* l_Lean_Compiler_FFI_getInternalCFlags___boxed(lean_object*);
+lean_object* l_List_redLength___rarg(lean_object*);
+static lean_object* l_Lean_Compiler_FFI_getInternalCFlags___closed__6;
 static lean_object* l_Lean_Compiler_FFI_getCFlags___closed__4;
+lean_object* lean_array_get_size(lean_object*);
+uint8_t lean_usize_dec_lt(size_t, size_t);
+lean_object* lean_get_leanc_internal_flags(lean_object*);
+static lean_object* l_Lean_Compiler_FFI_getInternalCFlags___closed__3;
 static lean_object* l_Lean_Compiler_FFI_getCFlags___closed__3;
 static lean_object* l_Lean_Compiler_FFI_getLinkerFlags___closed__4;
+lean_object* lean_array_uset(lean_object*, size_t, lean_object*);
+LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Compiler_FFI_getInternalCFlags___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+static lean_object* l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__4;
 lean_object* l_String_splitOn(lean_object*, lean_object*);
+lean_object* l_List_toArrayAux___rarg(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l___private_Lean_Compiler_FFI_0__Lean_Compiler_FFI_getLeancExtraFlags___boxed(lean_object* x_1) {
 _start:
 {
@@ -130,6 +168,156 @@ x_7 = l_List_foldl___at_Array_appendList___spec__1___rarg(x_5, x_6);
 return x_7;
 }
 }
+LEAN_EXPORT lean_object* l___private_Lean_Compiler_FFI_0__Lean_Compiler_FFI_getLeancInternalFlags___boxed(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_get_leanc_internal_flags(x_1);
+return x_2;
+}
+}
+static lean_object* _init_l_Array_mapMUnsafe_map___at_Lean_Compiler_FFI_getInternalCFlags___spec__1___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string_unchecked("ROOT", 4, 4);
+return x_1;
+}
+}
+LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Compiler_FFI_getInternalCFlags___spec__1(lean_object* x_1, size_t x_2, size_t x_3, lean_object* x_4) {
+_start:
+{
+uint8_t x_5; 
+x_5 = lean_usize_dec_lt(x_3, x_2);
+if (x_5 == 0)
+{
+return x_4;
+}
+else
+{
+lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; size_t x_11; size_t x_12; lean_object* x_13; 
+x_6 = lean_array_uget(x_4, x_3);
+x_7 = lean_unsigned_to_nat(0u);
+x_8 = lean_array_uset(x_4, x_3, x_7);
+x_9 = l_Array_mapMUnsafe_map___at_Lean_Compiler_FFI_getInternalCFlags___spec__1___closed__1;
+x_10 = l_String_replace(x_6, x_9, x_1);
+lean_dec(x_6);
+x_11 = 1;
+x_12 = lean_usize_add(x_3, x_11);
+x_13 = lean_array_uset(x_8, x_3, x_10);
+x_3 = x_12;
+x_4 = x_13;
+goto _start;
+}
+}
+}
+static lean_object* _init_l_Lean_Compiler_FFI_getInternalCFlags___closed__1() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = lean_box(0);
+x_2 = lean_get_leanc_internal_flags(x_1);
+return x_2;
+}
+}
+static lean_object* _init_l_Lean_Compiler_FFI_getInternalCFlags___closed__2() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_Lean_Compiler_FFI_getInternalCFlags___closed__1;
+x_2 = l_String_trim(x_1);
+return x_2;
+}
+}
+static lean_object* _init_l_Lean_Compiler_FFI_getInternalCFlags___closed__3() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_Compiler_FFI_getInternalCFlags___closed__2;
+x_2 = l_Lean_Compiler_FFI_getCFlags___closed__7;
+x_3 = l_String_splitOn(x_1, x_2);
+return x_3;
+}
+}
+static lean_object* _init_l_Lean_Compiler_FFI_getInternalCFlags___closed__4() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_Lean_Compiler_FFI_getInternalCFlags___closed__3;
+x_2 = l_List_redLength___rarg(x_1);
+return x_2;
+}
+}
+static lean_object* _init_l_Lean_Compiler_FFI_getInternalCFlags___closed__5() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_Lean_Compiler_FFI_getInternalCFlags___closed__4;
+x_2 = lean_mk_empty_array_with_capacity(x_1);
+return x_2;
+}
+}
+static lean_object* _init_l_Lean_Compiler_FFI_getInternalCFlags___closed__6() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_Compiler_FFI_getInternalCFlags___closed__3;
+x_2 = l_Lean_Compiler_FFI_getInternalCFlags___closed__5;
+x_3 = l_List_toArrayAux___rarg(x_1, x_2);
+return x_3;
+}
+}
+static lean_object* _init_l_Lean_Compiler_FFI_getInternalCFlags___closed__7() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_Lean_Compiler_FFI_getInternalCFlags___closed__6;
+x_2 = lean_array_get_size(x_1);
+return x_2;
+}
+}
+static size_t _init_l_Lean_Compiler_FFI_getInternalCFlags___closed__8() {
+_start:
+{
+lean_object* x_1; size_t x_2; 
+x_1 = l_Lean_Compiler_FFI_getInternalCFlags___closed__7;
+x_2 = lean_usize_of_nat(x_1);
+return x_2;
+}
+}
+LEAN_EXPORT lean_object* l_Lean_Compiler_FFI_getInternalCFlags(lean_object* x_1) {
+_start:
+{
+size_t x_2; size_t x_3; lean_object* x_4; lean_object* x_5; 
+x_2 = 0;
+x_3 = l_Lean_Compiler_FFI_getInternalCFlags___closed__8;
+x_4 = l_Lean_Compiler_FFI_getInternalCFlags___closed__6;
+x_5 = l_Array_mapMUnsafe_map___at_Lean_Compiler_FFI_getInternalCFlags___spec__1(x_1, x_3, x_2, x_4);
+return x_5;
+}
+}
+LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Compiler_FFI_getInternalCFlags___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+size_t x_5; size_t x_6; lean_object* x_7; 
+x_5 = lean_unbox_usize(x_2);
+lean_dec(x_2);
+x_6 = lean_unbox_usize(x_3);
+lean_dec(x_3);
+x_7 = l_Array_mapMUnsafe_map___at_Lean_Compiler_FFI_getInternalCFlags___spec__1(x_1, x_5, x_6, x_4);
+lean_dec(x_1);
+return x_7;
+}
+}
+LEAN_EXPORT lean_object* l_Lean_Compiler_FFI_getInternalCFlags___boxed(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = l_Lean_Compiler_FFI_getInternalCFlags(x_1);
+lean_dec(x_1);
+return x_2;
+}
+}
 LEAN_EXPORT lean_object* l___private_Lean_Compiler_FFI_0__Lean_Compiler_FFI_getBuiltinLinkerFlags___boxed(lean_object* x_1) {
 _start:
 {
@@ -203,6 +391,148 @@ x_4 = l_Lean_Compiler_FFI_getLinkerFlags(x_1, x_3);
 return x_4;
 }
 }
+LEAN_EXPORT lean_object* l___private_Lean_Compiler_FFI_0__Lean_Compiler_FFI_getBuiltinInternalLinkerFlags___boxed(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_get_internal_linker_flags(x_1);
+return x_2;
+}
+}
+LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Compiler_FFI_getInternalLinkerFlags___spec__1(lean_object* x_1, size_t x_2, size_t x_3, lean_object* x_4) {
+_start:
+{
+uint8_t x_5; 
+x_5 = lean_usize_dec_lt(x_3, x_2);
+if (x_5 == 0)
+{
+return x_4;
+}
+else
+{
+lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; size_t x_11; size_t x_12; lean_object* x_13; 
+x_6 = lean_array_uget(x_4, x_3);
+x_7 = lean_unsigned_to_nat(0u);
+x_8 = lean_array_uset(x_4, x_3, x_7);
+x_9 = l_Array_mapMUnsafe_map___at_Lean_Compiler_FFI_getInternalCFlags___spec__1___closed__1;
+x_10 = l_String_replace(x_6, x_9, x_1);
+lean_dec(x_6);
+x_11 = 1;
+x_12 = lean_usize_add(x_3, x_11);
+x_13 = lean_array_uset(x_8, x_3, x_10);
+x_3 = x_12;
+x_4 = x_13;
+goto _start;
+}
+}
+}
+static lean_object* _init_l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__1() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = lean_box(0);
+x_2 = lean_get_internal_linker_flags(x_1);
+return x_2;
+}
+}
+static lean_object* _init_l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__2() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__1;
+x_2 = l_String_trim(x_1);
+return x_2;
+}
+}
+static lean_object* _init_l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__3() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__2;
+x_2 = l_Lean_Compiler_FFI_getCFlags___closed__7;
+x_3 = l_String_splitOn(x_1, x_2);
+return x_3;
+}
+}
+static lean_object* _init_l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__4() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__3;
+x_2 = l_List_redLength___rarg(x_1);
+return x_2;
+}
+}
+static lean_object* _init_l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__5() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__4;
+x_2 = lean_mk_empty_array_with_capacity(x_1);
+return x_2;
+}
+}
+static lean_object* _init_l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__6() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__3;
+x_2 = l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__5;
+x_3 = l_List_toArrayAux___rarg(x_1, x_2);
+return x_3;
+}
+}
+static lean_object* _init_l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__7() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__6;
+x_2 = lean_array_get_size(x_1);
+return x_2;
+}
+}
+static size_t _init_l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__8() {
+_start:
+{
+lean_object* x_1; size_t x_2; 
+x_1 = l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__7;
+x_2 = lean_usize_of_nat(x_1);
+return x_2;
+}
+}
+LEAN_EXPORT lean_object* l_Lean_Compiler_FFI_getInternalLinkerFlags(lean_object* x_1) {
+_start:
+{
+size_t x_2; size_t x_3; lean_object* x_4; lean_object* x_5; 
+x_2 = 0;
+x_3 = l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__8;
+x_4 = l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__6;
+x_5 = l_Array_mapMUnsafe_map___at_Lean_Compiler_FFI_getInternalLinkerFlags___spec__1(x_1, x_3, x_2, x_4);
+return x_5;
+}
+}
+LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Compiler_FFI_getInternalLinkerFlags___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+size_t x_5; size_t x_6; lean_object* x_7; 
+x_5 = lean_unbox_usize(x_2);
+lean_dec(x_2);
+x_6 = lean_unbox_usize(x_3);
+lean_dec(x_3);
+x_7 = l_Array_mapMUnsafe_map___at_Lean_Compiler_FFI_getInternalLinkerFlags___spec__1(x_1, x_5, x_6, x_4);
+lean_dec(x_1);
+return x_7;
+}
+}
+LEAN_EXPORT lean_object* l_Lean_Compiler_FFI_getInternalLinkerFlags___boxed(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = l_Lean_Compiler_FFI_getInternalLinkerFlags(x_1);
+lean_dec(x_1);
+return x_2;
+}
+}
 lean_object* initialize_Init_Data_Array_Basic(uint8_t builtin, lean_object*);
 lean_object* initialize_Init_System_FilePath(uint8_t builtin, lean_object*);
 static bool _G_initialized = false;
@@ -232,6 +562,23 @@ l_Lean_Compiler_FFI_getCFlags___closed__7 = _init_l_Lean_Compiler_FFI_getCFlags_
 lean_mark_persistent(l_Lean_Compiler_FFI_getCFlags___closed__7);
 l_Lean_Compiler_FFI_getCFlags___closed__8 = _init_l_Lean_Compiler_FFI_getCFlags___closed__8();
 lean_mark_persistent(l_Lean_Compiler_FFI_getCFlags___closed__8);
+l_Array_mapMUnsafe_map___at_Lean_Compiler_FFI_getInternalCFlags___spec__1___closed__1 = _init_l_Array_mapMUnsafe_map___at_Lean_Compiler_FFI_getInternalCFlags___spec__1___closed__1();
+lean_mark_persistent(l_Array_mapMUnsafe_map___at_Lean_Compiler_FFI_getInternalCFlags___spec__1___closed__1);
+l_Lean_Compiler_FFI_getInternalCFlags___closed__1 = _init_l_Lean_Compiler_FFI_getInternalCFlags___closed__1();
+lean_mark_persistent(l_Lean_Compiler_FFI_getInternalCFlags___closed__1);
+l_Lean_Compiler_FFI_getInternalCFlags___closed__2 = _init_l_Lean_Compiler_FFI_getInternalCFlags___closed__2();
+lean_mark_persistent(l_Lean_Compiler_FFI_getInternalCFlags___closed__2);
+l_Lean_Compiler_FFI_getInternalCFlags___closed__3 = _init_l_Lean_Compiler_FFI_getInternalCFlags___closed__3();
+lean_mark_persistent(l_Lean_Compiler_FFI_getInternalCFlags___closed__3);
+l_Lean_Compiler_FFI_getInternalCFlags___closed__4 = _init_l_Lean_Compiler_FFI_getInternalCFlags___closed__4();
+lean_mark_persistent(l_Lean_Compiler_FFI_getInternalCFlags___closed__4);
+l_Lean_Compiler_FFI_getInternalCFlags___closed__5 = _init_l_Lean_Compiler_FFI_getInternalCFlags___closed__5();
+lean_mark_persistent(l_Lean_Compiler_FFI_getInternalCFlags___closed__5);
+l_Lean_Compiler_FFI_getInternalCFlags___closed__6 = _init_l_Lean_Compiler_FFI_getInternalCFlags___closed__6();
+lean_mark_persistent(l_Lean_Compiler_FFI_getInternalCFlags___closed__6);
+l_Lean_Compiler_FFI_getInternalCFlags___closed__7 = _init_l_Lean_Compiler_FFI_getInternalCFlags___closed__7();
+lean_mark_persistent(l_Lean_Compiler_FFI_getInternalCFlags___closed__7);
+l_Lean_Compiler_FFI_getInternalCFlags___closed__8 = _init_l_Lean_Compiler_FFI_getInternalCFlags___closed__8();
 l_Lean_Compiler_FFI_getLinkerFlags___closed__1 = _init_l_Lean_Compiler_FFI_getLinkerFlags___closed__1();
 lean_mark_persistent(l_Lean_Compiler_FFI_getLinkerFlags___closed__1);
 l_Lean_Compiler_FFI_getLinkerFlags___closed__2 = _init_l_Lean_Compiler_FFI_getLinkerFlags___closed__2();
@@ -240,6 +587,21 @@ l_Lean_Compiler_FFI_getLinkerFlags___closed__3 = _init_l_Lean_Compiler_FFI_getLi
 lean_mark_persistent(l_Lean_Compiler_FFI_getLinkerFlags___closed__3);
 l_Lean_Compiler_FFI_getLinkerFlags___closed__4 = _init_l_Lean_Compiler_FFI_getLinkerFlags___closed__4();
 lean_mark_persistent(l_Lean_Compiler_FFI_getLinkerFlags___closed__4);
+l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__1 = _init_l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__1();
+lean_mark_persistent(l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__1);
+l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__2 = _init_l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__2();
+lean_mark_persistent(l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__2);
+l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__3 = _init_l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__3();
+lean_mark_persistent(l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__3);
+l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__4 = _init_l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__4();
+lean_mark_persistent(l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__4);
+l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__5 = _init_l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__5();
+lean_mark_persistent(l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__5);
+l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__6 = _init_l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__6();
+lean_mark_persistent(l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__6);
+l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__7 = _init_l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__7();
+lean_mark_persistent(l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__7);
+l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__8 = _init_l_Lean_Compiler_FFI_getInternalLinkerFlags___closed__8();
 return lean_io_result_mk_ok(lean_box(0));
 }
 #ifdef __cplusplus
diff --git a/stage0/stdlib/Lean/Elab/Inductive.c b/stage0/stdlib/Lean/Elab/Inductive.c
index 83433fa9aa..6bbc5c9695 100644
--- a/stage0/stdlib/Lean/Elab/Inductive.c
+++ b/stage0/stdlib/Lean/Elab/Inductive.c
@@ -713,7 +713,6 @@ LEAN_EXPORT lean_object* l_Subarray_forInUnsafe_loop___at___private_Lean_Elab_In
 LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Inductive_0__Lean_Elab_Command_applyDerivingHandlers___spec__4(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_forallBoundedTelescope___at_Lean_Elab_Term_addAutoBoundImplicits_x27___spec__2___rarg(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at_Lean_Elab_Command_accLevel_go___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_mkRecOn(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_addMessageContextFull___at_Lean_Meta_instAddMessageContextMetaM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_mkTypeFor___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Inductive_0__Lean_Elab_Command_checkNumParams___spec__1___closed__2;
@@ -940,6 +939,7 @@ lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_instantiateForallAux(lean_
 static lean_object* l_Lean_Elab_Command_shouldInferResultUniverse___closed__1;
 static lean_object* l_Lean_Elab_Command_checkValidInductiveModifier___rarg___lambda__1___closed__2;
 LEAN_EXPORT lean_object* l_Lean_Meta_forallTelescopeReducing___at___private_Lean_Elab_Inductive_0__Lean_Elab_Command_collectUniverses_go___spec__2___rarg(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_mkRecOn(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_elabCtors_checkParamOccs___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_fixedIndicesToParams___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Std_Range_forIn_loop___at___private_Lean_Elab_Inductive_0__Lean_Elab_Command_elabCtors_checkParamOccs___spec__1___closed__4;
@@ -21776,8 +21776,10 @@ lean_inc(x_19);
 lean_dec(x_18);
 lean_inc(x_14);
 lean_inc(x_13);
+lean_inc(x_12);
+lean_inc(x_11);
 lean_inc(x_19);
-x_20 = l_Lean_mkRecOn(x_19, x_11, x_12, x_13, x_14, x_15);
+x_20 = l_mkRecOn(x_19, x_11, x_12, x_13, x_14, x_15);
 if (lean_obj_tag(x_20) == 0)
 {
 if (x_3 == 0)
diff --git a/stage0/stdlib/Lean/Elab/Structure.c b/stage0/stdlib/Lean/Elab/Structure.c
index b2c0211545..3f139747c7 100644
--- a/stage0/stdlib/Lean/Elab/Structure.c
+++ b/stage0/stdlib/Lean/Elab/Structure.c
@@ -689,6 +689,7 @@ lean_object* l_Lean_Elab_Term_addTermInfo_x27(lean_object*, lean_object*, lean_o
 lean_object* l_Lean_FileMap_leanPosToLspPos(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_levelMVarToParam___spec__1(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Elab_Command_elabStructure___lambda__2___boxed(lean_object**);
+lean_object* l_Lean_setReducibilityStatus___at_mkRecOn___spec__3(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Elab_elabAttr___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__4___lambda__1___closed__1;
 LEAN_EXPORT lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_copyDefaultValue_x3f_failed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabFieldTypeValue(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -807,7 +808,6 @@ LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Stru
 static lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_copyDefaultValue_x3f_go_x3f___closed__2;
 static lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Structure___hyg_13419____closed__3;
 static lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_processSubfields_go___rarg___closed__5;
-lean_object* l_Lean_mkRecOn(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_addMessageContextFull___at_Lean_Meta_instAddMessageContextMetaM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__5___lambda__1(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Structure___hyg_13419____closed__2;
@@ -1012,7 +1012,7 @@ LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Stru
 lean_object* l_Lean_MessageData_ofName(lean_object*);
 lean_object* lean_expr_instantiate1(lean_object*, lean_object*);
 uint8_t l_Lean_Elab_Modifiers_isPartial(lean_object*);
-lean_object* l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_mkRecOn(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_copyNewFieldsFrom_copyFields_copy___rarg___closed__7;
 static lean_object* l_Lean_Elab_elabModifiers___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__1___closed__1;
 LEAN_EXPORT lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_getFieldType___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -25640,8 +25640,10 @@ x_17 = l___private_Lean_Elab_Structure_0__Lean_Elab_Command_mkAuxConstructions__
 x_18 = l_Lean_Environment_contains(x_12, x_17);
 lean_inc(x_7);
 lean_inc(x_6);
+lean_inc(x_5);
+lean_inc(x_4);
 lean_inc(x_1);
-x_19 = l_Lean_mkRecOn(x_1, x_4, x_5, x_6, x_7, x_11);
+x_19 = l_mkRecOn(x_1, x_4, x_5, x_6, x_7, x_11);
 if (lean_obj_tag(x_19) == 0)
 {
 if (x_14 == 0)
@@ -27555,7 +27557,7 @@ if (x_52 == 0)
 {
 uint8_t x_53; lean_object* x_54; 
 x_53 = 0;
-x_54 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4(x_41, x_53, x_13, x_14, x_15, x_16, x_51);
+x_54 = l_Lean_setReducibilityStatus___at_mkRecOn___spec__3(x_41, x_53, x_13, x_14, x_15, x_16, x_51);
 lean_dec(x_16);
 lean_dec(x_15);
 lean_dec(x_14);
@@ -27626,7 +27628,7 @@ if (x_68 == 0)
 {
 uint8_t x_69; lean_object* x_70; 
 x_69 = 0;
-x_70 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4(x_41, x_69, x_13, x_14, x_15, x_16, x_67);
+x_70 = l_Lean_setReducibilityStatus___at_mkRecOn___spec__3(x_41, x_69, x_13, x_14, x_15, x_16, x_67);
 lean_dec(x_16);
 lean_dec(x_15);
 lean_dec(x_14);
@@ -27767,7 +27769,7 @@ if (x_101 == 0)
 {
 uint8_t x_102; lean_object* x_103; 
 x_102 = 0;
-x_103 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4(x_89, x_102, x_13, x_14, x_15, x_16, x_100);
+x_103 = l_Lean_setReducibilityStatus___at_mkRecOn___spec__3(x_89, x_102, x_13, x_14, x_15, x_16, x_100);
 lean_dec(x_16);
 lean_dec(x_15);
 lean_dec(x_14);
@@ -27840,7 +27842,7 @@ if (x_117 == 0)
 {
 uint8_t x_118; lean_object* x_119; 
 x_118 = 0;
-x_119 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4(x_89, x_118, x_13, x_14, x_15, x_16, x_116);
+x_119 = l_Lean_setReducibilityStatus___at_mkRecOn___spec__3(x_89, x_118, x_13, x_14, x_15, x_16, x_116);
 lean_dec(x_16);
 lean_dec(x_15);
 lean_dec(x_14);
diff --git a/stage0/stdlib/Lean/Meta/Constructions.c b/stage0/stdlib/Lean/Meta/Constructions.c
index 84cb44fe55..39c810663f 100644
--- a/stage0/stdlib/Lean/Meta/Constructions.c
+++ b/stage0/stdlib/Lean/Meta/Constructions.c
@@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: Lean.Meta.Constructions
-// Imports: Lean.AuxRecursor Lean.AddDecl Lean.Meta.AppBuilder Lean.Meta.CompletionName
+// Imports: Lean.AuxRecursor Lean.AddDecl Lean.Meta.AppBuilder Lean.Meta.CompletionName Lean.Meta.Constructions.RecOn
 #include <lean/lean.h>
 #if defined(__clang__)
 #pragma clang diagnostic ignored "-Wunused-parameter"
@@ -19,56 +19,55 @@ lean_object* l_Lean_Expr_const___override(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l___private_Lean_Meta_Constructions_0__Lean_mkBelowOrIBelow___lambda__1(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_mk_below(lean_object*, lean_object*, uint8_t);
 lean_object* l_Lean_mkNatLit(lean_object*);
+static lean_object* l_Lean_mkCasesOn___closed__7;
 lean_object* l_Lean_getConstInfo___at_Lean_Meta_mkConstWithFreshMVarLevels___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_mkAppOptM(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_mkBelowImp___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* lean_mk_empty_array_with_capacity(lean_object*);
 lean_object* l_Lean_mkAppN(lean_object*, lean_object*);
+static lean_object* l_Lean_mkCasesOn___closed__6;
 static lean_object* l_Lean_mkNoConfusionEnum_mkToCtorIdx___closed__11;
+LEAN_EXPORT lean_object* l_Lean_ofExceptKernelException___at_Lean_mkCasesOn___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_mkNoConfusionCore___lambda__1___closed__3;
 LEAN_EXPORT lean_object* l___private_Lean_Meta_Constructions_0__Lean_mkBRecOrBInductionOn___lambda__2(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_ConstantInfo_levelParams(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_mkBRecOnImp___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_mkAppB(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_List_allM___at_Lean_mkNoConfusion___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+static lean_object* l_Lean_mkCasesOn___closed__2;
 static lean_object* l_Lean_mkNoConfusionEnum_mkToCtorIdx___closed__8;
 static lean_object* l_Lean_mkNoConfusionEnum_mkNoConfusionType___closed__2;
 static lean_object* l_Lean_mkNoConfusionEnum_mkToCtorIdx___lambda__1___closed__1;
 lean_object* l_Lean_Expr_sort___override(lean_object*);
+static lean_object* l_Lean_mkCasesOn___closed__3;
 lean_object* lean_array_push(lean_object*, lean_object*);
 static lean_object* l_Lean_mkNoConfusionEnum_mkNoConfusion___lambda__1___closed__6;
-static lean_object* l_Lean_mkRecOn___closed__1;
 static lean_object* l_Lean_mkNoConfusionEnum_mkToCtorIdx___closed__6;
-LEAN_EXPORT lean_object* l_Lean_throwKernelException___at_Lean_mkRecOn___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_mkNoConfusionTypeCoreImp___boxed(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_isEnumType___at_Lean_mkNoConfusion___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_casesOnSuffix;
-static lean_object* l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__4;
+LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_mkCasesOn___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l___private_Lean_Meta_Constructions_0__Lean_mkBRecOrBInductionOn___lambda__2___closed__1;
 extern lean_object* l_Lean_auxRecExt;
 static lean_object* l_Lean_mkNoConfusionEnum_mkNoConfusion___lambda__2___closed__1;
 LEAN_EXPORT lean_object* l_Lean_mkNoConfusionEnum_mkNoConfusion___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_mkBelow(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-static lean_object* l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__5;
+LEAN_EXPORT lean_object* l_Lean_throwKernelException___at_Lean_mkCasesOn___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_mkNoConfusionEnum_mkNoConfusionType___lambda__2___closed__2;
 LEAN_EXPORT lean_object* l_Lean_mkBRecOn(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Lean_mkRecOnImp___boxed(lean_object*, lean_object*);
 static lean_object* l_Lean_mkNoConfusionCore___lambda__1___closed__1;
 LEAN_EXPORT lean_object* l_Lean_mkNoConfusionCore___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_mkNoConfusionEnum_mkNoConfusionType___lambda__1___closed__1;
 static lean_object* l_Lean_mkNoConfusionEnum_mkNoConfusionType___closed__6;
 LEAN_EXPORT lean_object* l_Lean_mkNoConfusionCore___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_st_ref_take(lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Lean_ofExceptKernelException___at_Lean_mkRecOn___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l___private_Lean_Meta_Constructions_0__Lean_mkBelowOrIBelow___lambda__2(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Lean_throwKernelException___at_Lean_mkRecOn___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_mkNoConfusionEnum_mkNoConfusionType___closed__4;
 LEAN_EXPORT lean_object* l___private_Lean_Meta_Constructions_0__Lean_mkBRecOrBInductionOn___lambda__1(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l___private_Lean_Meta_Constructions_0__Lean_mkBRecOrBInductionOn___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_mkNoConfusionEnum_mkNoConfusion___closed__1;
-static lean_object* l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__1;
+LEAN_EXPORT lean_object* l_Lean_throwKernelException___at_Lean_mkCasesOn___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_CoreM_0__Lean_Core_mkFreshNameImp(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_mkCasesOn(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Declaration_definitionVal_x21(lean_object*);
@@ -82,6 +81,7 @@ lean_object* l_Lean_Meta_mkAppM(lean_object*, lean_object*, lean_object*, lean_o
 uint8_t l_List_isEmpty___rarg(lean_object*);
 static lean_object* l_Lean_mkNoConfusionEnum_mkToCtorIdx___closed__10;
 lean_object* l_Lean_Meta_mkEq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_mkCasesOn___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_mkNoConfusionCoreImp___boxed(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_mkNoConfusionEnum_mkNoConfusion___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_mkCasesOnImp___boxed(lean_object*, lean_object*);
@@ -93,16 +93,13 @@ LEAN_EXPORT lean_object* l___private_Lean_Meta_Constructions_0__Lean_mkBRecOrBIn
 lean_object* l_Lean_Name_str___override(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_List_allM___at_Lean_mkNoConfusion___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Util_0__mkPanicMessageWithDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Lean_ofExceptKernelException___at_Lean_mkCasesOn___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_mkNoConfusionEnum_mkNoConfusionType___lambda__1___closed__4;
 static lean_object* l_Lean_mkNoConfusionEnum_mkToCtorIdx___closed__7;
-lean_object* l___private_Lean_ReducibilityAttrs_0__Lean_setReducibilityStatusCore(lean_object*, lean_object*, uint8_t, uint8_t, lean_object*);
-LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_mkRecOn___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-static lean_object* l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__3;
 LEAN_EXPORT lean_object* l_Lean_isEnumType___at_Lean_mkNoConfusion___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_mkNoConfusionEnum_mkToCtorIdx___closed__2;
 LEAN_EXPORT lean_object* l_Lean_mkNoConfusionEnum_mkNoConfusion(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_panic___at_Lean_mkNoConfusionEnum_mkToCtorIdx___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-extern lean_object* l_Lean_recOnSuffix;
 lean_object* l_Lean_Meta_instInhabitedMetaM___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_Environment_contains(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l___private_Lean_Meta_Constructions_0__Lean_mkBRecOrBInductionOn___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -118,6 +115,7 @@ LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at_Lean_mkNoConfusionEnum_mkTo
 LEAN_EXPORT lean_object* l_Lean_mkNoConfusionEnum(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_mkNoConfusionEnum_mkNoConfusionType___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_mkNoConfusionEnum_mkNoConfusionType___lambda__2___closed__1;
+lean_object* l_Lean_setReducibilityStatus___at_mkRecOn___spec__3(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_mkNoConfusionEnum_mkToCtorIdx___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_mkNoConfusionEnum_mkNoConfusionType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_mkNoConfusion(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -129,17 +127,13 @@ static lean_object* l_Lean_mkNoConfusionEnum_mkNoConfusionType___lambda__1___clo
 LEAN_EXPORT lean_object* l___private_Lean_Meta_Constructions_0__Lean_mkBRecOrBInductionOn___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Meta_completionBlackListExt;
 uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
-static lean_object* l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__2;
 LEAN_EXPORT lean_object* l_Lean_mkNoConfusionEnum_mkToCtorIdx(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Lean_ofExceptKernelException___at_Lean_mkRecOn___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_TagDeclarationExtension_tag(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_mkForallFVars(lean_object*, lean_object*, uint8_t, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l___private_Lean_Meta_Constructions_0__Lean_mkBRecOrBInductionOn___lambda__3(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_mkNoConfusionEnum_mkNoConfusionType___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Lean_mkRecOn(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_addMessageContextFull___at_Lean_Meta_instAddMessageContextMetaM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_mkCasesOn___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* lean_mk_rec_on(lean_object*, lean_object*);
 lean_object* lean_panic_fn(lean_object*, lean_object*);
 static lean_object* l_Lean_mkNoConfusionEnum_mkNoConfusion___lambda__2___closed__2;
 lean_object* lean_nat_sub(lean_object*, lean_object*);
@@ -153,13 +147,13 @@ extern lean_object* l_Lean_noConfusionExt;
 lean_object* l_Lean_Meta_withLocalDecl___at___private_Lean_Meta_SynthInstance_0__Lean_Meta_SynthInstance_removeUnusedArguments_x3f___spec__2___rarg(lean_object*, uint8_t, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Level_param___override(lean_object*);
 LEAN_EXPORT lean_object* l___private_Lean_Meta_Constructions_0__Lean_mkBelowOrIBelow___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+static lean_object* l_Lean_mkCasesOn___closed__1;
 lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
-static lean_object* l_Lean_mkRecOn___closed__2;
 LEAN_EXPORT lean_object* l___private_Lean_Meta_Constructions_0__Lean_mkBelowOrIBelow___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+static lean_object* l_Lean_mkCasesOn___closed__5;
 lean_object* l_List_map___at_Lean_mkConstWithLevelParams___spec__1(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_mkBInductionOn(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_mkNoConfusionCore(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_mkRecOn___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_mkNoConfusionEnum_mkToCtorIdx___closed__4;
 uint8_t lean_nat_dec_le(lean_object*, lean_object*);
 lean_object* l_Lean_Meta_mkLambdaFVars(lean_object*, lean_object*, uint8_t, uint8_t, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -168,27 +162,17 @@ lean_object* l_Lean_addAndCompile(lean_object*, lean_object*, lean_object*, lean
 lean_object* lean_nat_add(lean_object*, lean_object*);
 static lean_object* l_Lean_mkNoConfusionEnum_mkToCtorIdx___closed__9;
 static lean_object* l_Lean_mkNoConfusionEnum_mkNoConfusionType___lambda__1___closed__3;
-LEAN_EXPORT lean_object* l_Lean_mkRecOn___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_KernelException_toMessageData(lean_object*, lean_object*);
 static lean_object* l_Lean_mkNoConfusionEnum_mkToCtorIdx___closed__3;
-LEAN_EXPORT lean_object* l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_mk_brec_on(lean_object*, lean_object*, uint8_t);
 LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at_Lean_mkNoConfusionEnum_mkToCtorIdx___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+static lean_object* l_Lean_mkCasesOn___closed__4;
 static lean_object* l_Lean_mkNoConfusionEnum_mkNoConfusion___closed__2;
 LEAN_EXPORT lean_object* l___private_Lean_Meta_Constructions_0__Lean_mkBelowOrIBelow(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_addDecl(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_mk_cases_on(lean_object*, lean_object*);
 lean_object* l_List_length___rarg(lean_object*);
 static lean_object* l_Lean_mkNoConfusionEnum_mkNoConfusion___lambda__1___closed__3;
-LEAN_EXPORT lean_object* l_Lean_mkRecOnImp___boxed(lean_object* x_1, lean_object* x_2) {
-_start:
-{
-lean_object* x_3; 
-x_3 = lean_mk_rec_on(x_1, x_2);
-lean_dec(x_2);
-return x_3;
-}
-}
 LEAN_EXPORT lean_object* l_Lean_mkCasesOnImp___boxed(lean_object* x_1, lean_object* x_2) {
 _start:
 {
@@ -238,7 +222,7 @@ lean_dec(x_2);
 return x_5;
 }
 }
-LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_mkRecOn___spec__3(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
+LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_mkCasesOn___spec__3(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
 _start:
 {
 lean_object* x_7; lean_object* x_8; uint8_t x_9; 
@@ -276,19 +260,19 @@ return x_15;
 }
 }
 }
-LEAN_EXPORT lean_object* l_Lean_throwKernelException___at_Lean_mkRecOn___spec__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
+LEAN_EXPORT lean_object* l_Lean_throwKernelException___at_Lean_mkCasesOn___spec__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
 _start:
 {
 lean_object* x_7; lean_object* x_8; lean_object* x_9; 
 x_7 = lean_ctor_get(x_4, 2);
 lean_inc(x_7);
 x_8 = l_Lean_KernelException_toMessageData(x_1, x_7);
-x_9 = l_Lean_throwError___at_Lean_mkRecOn___spec__3(x_8, x_2, x_3, x_4, x_5, x_6);
+x_9 = l_Lean_throwError___at_Lean_mkCasesOn___spec__3(x_8, x_2, x_3, x_4, x_5, x_6);
 lean_dec(x_4);
 return x_9;
 }
 }
-LEAN_EXPORT lean_object* l_Lean_ofExceptKernelException___at_Lean_mkRecOn___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
+LEAN_EXPORT lean_object* l_Lean_ofExceptKernelException___at_Lean_mkCasesOn___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
 _start:
 {
 if (lean_obj_tag(x_1) == 0)
@@ -297,7 +281,7 @@ lean_object* x_7; lean_object* x_8;
 x_7 = lean_ctor_get(x_1, 0);
 lean_inc(x_7);
 lean_dec(x_1);
-x_8 = l_Lean_throwKernelException___at_Lean_mkRecOn___spec__2(x_7, x_2, x_3, x_4, x_5, x_6);
+x_8 = l_Lean_throwKernelException___at_Lean_mkCasesOn___spec__2(x_7, x_2, x_3, x_4, x_5, x_6);
 return x_8;
 }
 else
@@ -314,7 +298,15 @@ return x_10;
 }
 }
 }
-static lean_object* _init_l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__1() {
+static lean_object* _init_l_Lean_mkCasesOn___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = l_Lean_auxRecExt;
+return x_1;
+}
+}
+static lean_object* _init_l_Lean_mkCasesOn___closed__2() {
 _start:
 {
 lean_object* x_1; 
@@ -322,32 +314,32 @@ x_1 = l_Lean_PersistentHashMap_mkEmptyEntriesArray(lean_box(0), lean_box(0));
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__2() {
+static lean_object* _init_l_Lean_mkCasesOn___closed__3() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; 
-x_1 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__1;
+x_1 = l_Lean_mkCasesOn___closed__2;
 x_2 = lean_alloc_ctor(0, 1, 0);
 lean_ctor_set(x_2, 0, x_1);
 return x_2;
 }
 }
-static lean_object* _init_l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__3() {
+static lean_object* _init_l_Lean_mkCasesOn___closed__4() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; 
-x_1 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__2;
+x_1 = l_Lean_mkCasesOn___closed__3;
 x_2 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_2, 0, x_1);
 lean_ctor_set(x_2, 1, x_1);
 return x_2;
 }
 }
-static lean_object* _init_l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__4() {
+static lean_object* _init_l_Lean_mkCasesOn___closed__5() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; 
-x_1 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__2;
+x_1 = l_Lean_mkCasesOn___closed__3;
 x_2 = lean_alloc_ctor(0, 4, 0);
 lean_ctor_set(x_2, 0, x_1);
 lean_ctor_set(x_2, 1, x_1);
@@ -356,12 +348,12 @@ lean_ctor_set(x_2, 3, x_1);
 return x_2;
 }
 }
-static lean_object* _init_l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__5() {
+static lean_object* _init_l_Lean_mkCasesOn___closed__6() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__2;
-x_2 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__4;
+x_1 = l_Lean_mkCasesOn___closed__3;
+x_2 = l_Lean_mkCasesOn___closed__5;
 x_3 = lean_alloc_ctor(0, 7, 0);
 lean_ctor_set(x_3, 0, x_1);
 lean_ctor_set(x_3, 1, x_1);
@@ -373,212 +365,7 @@ lean_ctor_set(x_3, 6, x_2);
 return x_3;
 }
 }
-LEAN_EXPORT lean_object* l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4(lean_object* x_1, uint8_t x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
-_start:
-{
-lean_object* x_8; lean_object* x_9; lean_object* x_10; uint8_t x_11; 
-x_8 = lean_st_ref_take(x_6, x_7);
-x_9 = lean_ctor_get(x_8, 0);
-lean_inc(x_9);
-x_10 = lean_ctor_get(x_8, 1);
-lean_inc(x_10);
-lean_dec(x_8);
-x_11 = !lean_is_exclusive(x_9);
-if (x_11 == 0)
-{
-lean_object* x_12; lean_object* x_13; uint8_t x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; uint8_t x_23; 
-x_12 = lean_ctor_get(x_9, 0);
-x_13 = lean_ctor_get(x_9, 4);
-lean_dec(x_13);
-x_14 = 0;
-x_15 = lean_box(0);
-x_16 = l___private_Lean_ReducibilityAttrs_0__Lean_setReducibilityStatusCore(x_12, x_1, x_2, x_14, x_15);
-x_17 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__3;
-lean_ctor_set(x_9, 4, x_17);
-lean_ctor_set(x_9, 0, x_16);
-x_18 = lean_st_ref_set(x_6, x_9, x_10);
-x_19 = lean_ctor_get(x_18, 1);
-lean_inc(x_19);
-lean_dec(x_18);
-x_20 = lean_st_ref_take(x_4, x_19);
-x_21 = lean_ctor_get(x_20, 0);
-lean_inc(x_21);
-x_22 = lean_ctor_get(x_20, 1);
-lean_inc(x_22);
-lean_dec(x_20);
-x_23 = !lean_is_exclusive(x_21);
-if (x_23 == 0)
-{
-lean_object* x_24; lean_object* x_25; lean_object* x_26; uint8_t x_27; 
-x_24 = lean_ctor_get(x_21, 1);
-lean_dec(x_24);
-x_25 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__5;
-lean_ctor_set(x_21, 1, x_25);
-x_26 = lean_st_ref_set(x_4, x_21, x_22);
-x_27 = !lean_is_exclusive(x_26);
-if (x_27 == 0)
-{
-lean_object* x_28; lean_object* x_29; 
-x_28 = lean_ctor_get(x_26, 0);
-lean_dec(x_28);
-x_29 = lean_box(0);
-lean_ctor_set(x_26, 0, x_29);
-return x_26;
-}
-else
-{
-lean_object* x_30; lean_object* x_31; lean_object* x_32; 
-x_30 = lean_ctor_get(x_26, 1);
-lean_inc(x_30);
-lean_dec(x_26);
-x_31 = lean_box(0);
-x_32 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_32, 0, x_31);
-lean_ctor_set(x_32, 1, x_30);
-return x_32;
-}
-}
-else
-{
-lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; 
-x_33 = lean_ctor_get(x_21, 0);
-x_34 = lean_ctor_get(x_21, 2);
-x_35 = lean_ctor_get(x_21, 3);
-x_36 = lean_ctor_get(x_21, 4);
-lean_inc(x_36);
-lean_inc(x_35);
-lean_inc(x_34);
-lean_inc(x_33);
-lean_dec(x_21);
-x_37 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__5;
-x_38 = lean_alloc_ctor(0, 5, 0);
-lean_ctor_set(x_38, 0, x_33);
-lean_ctor_set(x_38, 1, x_37);
-lean_ctor_set(x_38, 2, x_34);
-lean_ctor_set(x_38, 3, x_35);
-lean_ctor_set(x_38, 4, x_36);
-x_39 = lean_st_ref_set(x_4, x_38, x_22);
-x_40 = lean_ctor_get(x_39, 1);
-lean_inc(x_40);
-if (lean_is_exclusive(x_39)) {
- lean_ctor_release(x_39, 0);
- lean_ctor_release(x_39, 1);
- x_41 = x_39;
-} else {
- lean_dec_ref(x_39);
- x_41 = lean_box(0);
-}
-x_42 = lean_box(0);
-if (lean_is_scalar(x_41)) {
- x_43 = lean_alloc_ctor(0, 2, 0);
-} else {
- x_43 = x_41;
-}
-lean_ctor_set(x_43, 0, x_42);
-lean_ctor_set(x_43, 1, x_40);
-return x_43;
-}
-}
-else
-{
-lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; uint8_t x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_71; 
-x_44 = lean_ctor_get(x_9, 0);
-x_45 = lean_ctor_get(x_9, 1);
-x_46 = lean_ctor_get(x_9, 2);
-x_47 = lean_ctor_get(x_9, 3);
-x_48 = lean_ctor_get(x_9, 5);
-x_49 = lean_ctor_get(x_9, 6);
-lean_inc(x_49);
-lean_inc(x_48);
-lean_inc(x_47);
-lean_inc(x_46);
-lean_inc(x_45);
-lean_inc(x_44);
-lean_dec(x_9);
-x_50 = 0;
-x_51 = lean_box(0);
-x_52 = l___private_Lean_ReducibilityAttrs_0__Lean_setReducibilityStatusCore(x_44, x_1, x_2, x_50, x_51);
-x_53 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__3;
-x_54 = lean_alloc_ctor(0, 7, 0);
-lean_ctor_set(x_54, 0, x_52);
-lean_ctor_set(x_54, 1, x_45);
-lean_ctor_set(x_54, 2, x_46);
-lean_ctor_set(x_54, 3, x_47);
-lean_ctor_set(x_54, 4, x_53);
-lean_ctor_set(x_54, 5, x_48);
-lean_ctor_set(x_54, 6, x_49);
-x_55 = lean_st_ref_set(x_6, x_54, x_10);
-x_56 = lean_ctor_get(x_55, 1);
-lean_inc(x_56);
-lean_dec(x_55);
-x_57 = lean_st_ref_take(x_4, x_56);
-x_58 = lean_ctor_get(x_57, 0);
-lean_inc(x_58);
-x_59 = lean_ctor_get(x_57, 1);
-lean_inc(x_59);
-lean_dec(x_57);
-x_60 = lean_ctor_get(x_58, 0);
-lean_inc(x_60);
-x_61 = lean_ctor_get(x_58, 2);
-lean_inc(x_61);
-x_62 = lean_ctor_get(x_58, 3);
-lean_inc(x_62);
-x_63 = lean_ctor_get(x_58, 4);
-lean_inc(x_63);
-if (lean_is_exclusive(x_58)) {
- lean_ctor_release(x_58, 0);
- lean_ctor_release(x_58, 1);
- lean_ctor_release(x_58, 2);
- lean_ctor_release(x_58, 3);
- lean_ctor_release(x_58, 4);
- x_64 = x_58;
-} else {
- lean_dec_ref(x_58);
- x_64 = lean_box(0);
-}
-x_65 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__5;
-if (lean_is_scalar(x_64)) {
- x_66 = lean_alloc_ctor(0, 5, 0);
-} else {
- x_66 = x_64;
-}
-lean_ctor_set(x_66, 0, x_60);
-lean_ctor_set(x_66, 1, x_65);
-lean_ctor_set(x_66, 2, x_61);
-lean_ctor_set(x_66, 3, x_62);
-lean_ctor_set(x_66, 4, x_63);
-x_67 = lean_st_ref_set(x_4, x_66, x_59);
-x_68 = lean_ctor_get(x_67, 1);
-lean_inc(x_68);
-if (lean_is_exclusive(x_67)) {
- lean_ctor_release(x_67, 0);
- lean_ctor_release(x_67, 1);
- x_69 = x_67;
-} else {
- lean_dec_ref(x_67);
- x_69 = lean_box(0);
-}
-x_70 = lean_box(0);
-if (lean_is_scalar(x_69)) {
- x_71 = lean_alloc_ctor(0, 2, 0);
-} else {
- x_71 = x_69;
-}
-lean_ctor_set(x_71, 0, x_70);
-lean_ctor_set(x_71, 1, x_68);
-return x_71;
-}
-}
-}
-static lean_object* _init_l_Lean_mkRecOn___closed__1() {
-_start:
-{
-lean_object* x_1; 
-x_1 = l_Lean_auxRecExt;
-return x_1;
-}
-}
-static lean_object* _init_l_Lean_mkRecOn___closed__2() {
+static lean_object* _init_l_Lean_mkCasesOn___closed__7() {
 _start:
 {
 lean_object* x_1; 
@@ -586,698 +373,6 @@ x_1 = l_Lean_protectedExt;
 return x_1;
 }
 }
-LEAN_EXPORT lean_object* l_Lean_mkRecOn(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
-_start:
-{
-lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; 
-x_7 = l_Lean_recOnSuffix;
-lean_inc(x_1);
-x_8 = l_Lean_Name_str___override(x_1, x_7);
-x_9 = lean_st_ref_get(x_5, x_6);
-x_10 = lean_ctor_get(x_9, 0);
-lean_inc(x_10);
-x_11 = lean_ctor_get(x_9, 1);
-lean_inc(x_11);
-lean_dec(x_9);
-x_12 = lean_ctor_get(x_10, 0);
-lean_inc(x_12);
-lean_dec(x_10);
-x_13 = lean_mk_rec_on(x_12, x_1);
-lean_dec(x_1);
-lean_inc(x_4);
-x_14 = l_Lean_ofExceptKernelException___at_Lean_mkRecOn___spec__1(x_13, x_2, x_3, x_4, x_5, x_11);
-if (lean_obj_tag(x_14) == 0)
-{
-lean_object* x_15; lean_object* x_16; lean_object* x_17; 
-x_15 = lean_ctor_get(x_14, 0);
-lean_inc(x_15);
-x_16 = lean_ctor_get(x_14, 1);
-lean_inc(x_16);
-lean_dec(x_14);
-lean_inc(x_5);
-lean_inc(x_4);
-x_17 = l_Lean_addDecl(x_15, x_4, x_5, x_16);
-if (lean_obj_tag(x_17) == 0)
-{
-lean_object* x_18; uint8_t x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; uint8_t x_25; 
-x_18 = lean_ctor_get(x_17, 1);
-lean_inc(x_18);
-lean_dec(x_17);
-x_19 = 0;
-lean_inc(x_8);
-x_20 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4(x_8, x_19, x_2, x_3, x_4, x_5, x_18);
-lean_dec(x_4);
-x_21 = lean_ctor_get(x_20, 1);
-lean_inc(x_21);
-lean_dec(x_20);
-x_22 = lean_st_ref_take(x_5, x_21);
-x_23 = lean_ctor_get(x_22, 0);
-lean_inc(x_23);
-x_24 = lean_ctor_get(x_22, 1);
-lean_inc(x_24);
-lean_dec(x_22);
-x_25 = !lean_is_exclusive(x_23);
-if (x_25 == 0)
-{
-lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; uint8_t x_36; 
-x_26 = lean_ctor_get(x_23, 0);
-x_27 = lean_ctor_get(x_23, 4);
-lean_dec(x_27);
-x_28 = l_Lean_mkRecOn___closed__1;
-lean_inc(x_8);
-x_29 = l_Lean_TagDeclarationExtension_tag(x_28, x_26, x_8);
-x_30 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__3;
-lean_ctor_set(x_23, 4, x_30);
-lean_ctor_set(x_23, 0, x_29);
-x_31 = lean_st_ref_set(x_5, x_23, x_24);
-x_32 = lean_ctor_get(x_31, 1);
-lean_inc(x_32);
-lean_dec(x_31);
-x_33 = lean_st_ref_take(x_3, x_32);
-x_34 = lean_ctor_get(x_33, 0);
-lean_inc(x_34);
-x_35 = lean_ctor_get(x_33, 1);
-lean_inc(x_35);
-lean_dec(x_33);
-x_36 = !lean_is_exclusive(x_34);
-if (x_36 == 0)
-{
-lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; uint8_t x_44; 
-x_37 = lean_ctor_get(x_34, 1);
-lean_dec(x_37);
-x_38 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__5;
-lean_ctor_set(x_34, 1, x_38);
-x_39 = lean_st_ref_set(x_3, x_34, x_35);
-x_40 = lean_ctor_get(x_39, 1);
-lean_inc(x_40);
-lean_dec(x_39);
-x_41 = lean_st_ref_take(x_5, x_40);
-x_42 = lean_ctor_get(x_41, 0);
-lean_inc(x_42);
-x_43 = lean_ctor_get(x_41, 1);
-lean_inc(x_43);
-lean_dec(x_41);
-x_44 = !lean_is_exclusive(x_42);
-if (x_44 == 0)
-{
-lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; uint8_t x_54; 
-x_45 = lean_ctor_get(x_42, 0);
-x_46 = lean_ctor_get(x_42, 4);
-lean_dec(x_46);
-x_47 = l_Lean_mkRecOn___closed__2;
-x_48 = l_Lean_TagDeclarationExtension_tag(x_47, x_45, x_8);
-lean_ctor_set(x_42, 4, x_30);
-lean_ctor_set(x_42, 0, x_48);
-x_49 = lean_st_ref_set(x_5, x_42, x_43);
-lean_dec(x_5);
-x_50 = lean_ctor_get(x_49, 1);
-lean_inc(x_50);
-lean_dec(x_49);
-x_51 = lean_st_ref_take(x_3, x_50);
-x_52 = lean_ctor_get(x_51, 0);
-lean_inc(x_52);
-x_53 = lean_ctor_get(x_51, 1);
-lean_inc(x_53);
-lean_dec(x_51);
-x_54 = !lean_is_exclusive(x_52);
-if (x_54 == 0)
-{
-lean_object* x_55; lean_object* x_56; uint8_t x_57; 
-x_55 = lean_ctor_get(x_52, 1);
-lean_dec(x_55);
-lean_ctor_set(x_52, 1, x_38);
-x_56 = lean_st_ref_set(x_3, x_52, x_53);
-x_57 = !lean_is_exclusive(x_56);
-if (x_57 == 0)
-{
-lean_object* x_58; lean_object* x_59; 
-x_58 = lean_ctor_get(x_56, 0);
-lean_dec(x_58);
-x_59 = lean_box(0);
-lean_ctor_set(x_56, 0, x_59);
-return x_56;
-}
-else
-{
-lean_object* x_60; lean_object* x_61; lean_object* x_62; 
-x_60 = lean_ctor_get(x_56, 1);
-lean_inc(x_60);
-lean_dec(x_56);
-x_61 = lean_box(0);
-x_62 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_62, 0, x_61);
-lean_ctor_set(x_62, 1, x_60);
-return x_62;
-}
-}
-else
-{
-lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_71; lean_object* x_72; 
-x_63 = lean_ctor_get(x_52, 0);
-x_64 = lean_ctor_get(x_52, 2);
-x_65 = lean_ctor_get(x_52, 3);
-x_66 = lean_ctor_get(x_52, 4);
-lean_inc(x_66);
-lean_inc(x_65);
-lean_inc(x_64);
-lean_inc(x_63);
-lean_dec(x_52);
-x_67 = lean_alloc_ctor(0, 5, 0);
-lean_ctor_set(x_67, 0, x_63);
-lean_ctor_set(x_67, 1, x_38);
-lean_ctor_set(x_67, 2, x_64);
-lean_ctor_set(x_67, 3, x_65);
-lean_ctor_set(x_67, 4, x_66);
-x_68 = lean_st_ref_set(x_3, x_67, x_53);
-x_69 = lean_ctor_get(x_68, 1);
-lean_inc(x_69);
-if (lean_is_exclusive(x_68)) {
- lean_ctor_release(x_68, 0);
- lean_ctor_release(x_68, 1);
- x_70 = x_68;
-} else {
- lean_dec_ref(x_68);
- x_70 = lean_box(0);
-}
-x_71 = lean_box(0);
-if (lean_is_scalar(x_70)) {
- x_72 = lean_alloc_ctor(0, 2, 0);
-} else {
- x_72 = x_70;
-}
-lean_ctor_set(x_72, 0, x_71);
-lean_ctor_set(x_72, 1, x_69);
-return x_72;
-}
-}
-else
-{
-lean_object* x_73; lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78; lean_object* x_79; lean_object* x_80; lean_object* x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86; lean_object* x_87; lean_object* x_88; lean_object* x_89; lean_object* x_90; lean_object* x_91; lean_object* x_92; lean_object* x_93; lean_object* x_94; lean_object* x_95; lean_object* x_96; lean_object* x_97; 
-x_73 = lean_ctor_get(x_42, 0);
-x_74 = lean_ctor_get(x_42, 1);
-x_75 = lean_ctor_get(x_42, 2);
-x_76 = lean_ctor_get(x_42, 3);
-x_77 = lean_ctor_get(x_42, 5);
-x_78 = lean_ctor_get(x_42, 6);
-lean_inc(x_78);
-lean_inc(x_77);
-lean_inc(x_76);
-lean_inc(x_75);
-lean_inc(x_74);
-lean_inc(x_73);
-lean_dec(x_42);
-x_79 = l_Lean_mkRecOn___closed__2;
-x_80 = l_Lean_TagDeclarationExtension_tag(x_79, x_73, x_8);
-x_81 = lean_alloc_ctor(0, 7, 0);
-lean_ctor_set(x_81, 0, x_80);
-lean_ctor_set(x_81, 1, x_74);
-lean_ctor_set(x_81, 2, x_75);
-lean_ctor_set(x_81, 3, x_76);
-lean_ctor_set(x_81, 4, x_30);
-lean_ctor_set(x_81, 5, x_77);
-lean_ctor_set(x_81, 6, x_78);
-x_82 = lean_st_ref_set(x_5, x_81, x_43);
-lean_dec(x_5);
-x_83 = lean_ctor_get(x_82, 1);
-lean_inc(x_83);
-lean_dec(x_82);
-x_84 = lean_st_ref_take(x_3, x_83);
-x_85 = lean_ctor_get(x_84, 0);
-lean_inc(x_85);
-x_86 = lean_ctor_get(x_84, 1);
-lean_inc(x_86);
-lean_dec(x_84);
-x_87 = lean_ctor_get(x_85, 0);
-lean_inc(x_87);
-x_88 = lean_ctor_get(x_85, 2);
-lean_inc(x_88);
-x_89 = lean_ctor_get(x_85, 3);
-lean_inc(x_89);
-x_90 = lean_ctor_get(x_85, 4);
-lean_inc(x_90);
-if (lean_is_exclusive(x_85)) {
- lean_ctor_release(x_85, 0);
- lean_ctor_release(x_85, 1);
- lean_ctor_release(x_85, 2);
- lean_ctor_release(x_85, 3);
- lean_ctor_release(x_85, 4);
- x_91 = x_85;
-} else {
- lean_dec_ref(x_85);
- x_91 = lean_box(0);
-}
-if (lean_is_scalar(x_91)) {
- x_92 = lean_alloc_ctor(0, 5, 0);
-} else {
- x_92 = x_91;
-}
-lean_ctor_set(x_92, 0, x_87);
-lean_ctor_set(x_92, 1, x_38);
-lean_ctor_set(x_92, 2, x_88);
-lean_ctor_set(x_92, 3, x_89);
-lean_ctor_set(x_92, 4, x_90);
-x_93 = lean_st_ref_set(x_3, x_92, x_86);
-x_94 = lean_ctor_get(x_93, 1);
-lean_inc(x_94);
-if (lean_is_exclusive(x_93)) {
- lean_ctor_release(x_93, 0);
- lean_ctor_release(x_93, 1);
- x_95 = x_93;
-} else {
- lean_dec_ref(x_93);
- x_95 = lean_box(0);
-}
-x_96 = lean_box(0);
-if (lean_is_scalar(x_95)) {
- x_97 = lean_alloc_ctor(0, 2, 0);
-} else {
- x_97 = x_95;
-}
-lean_ctor_set(x_97, 0, x_96);
-lean_ctor_set(x_97, 1, x_94);
-return x_97;
-}
-}
-else
-{
-lean_object* x_98; lean_object* x_99; lean_object* x_100; lean_object* x_101; lean_object* x_102; lean_object* x_103; lean_object* x_104; lean_object* x_105; lean_object* x_106; lean_object* x_107; lean_object* x_108; lean_object* x_109; lean_object* x_110; lean_object* x_111; lean_object* x_112; lean_object* x_113; lean_object* x_114; lean_object* x_115; lean_object* x_116; lean_object* x_117; lean_object* x_118; lean_object* x_119; lean_object* x_120; lean_object* x_121; lean_object* x_122; lean_object* x_123; lean_object* x_124; lean_object* x_125; lean_object* x_126; lean_object* x_127; lean_object* x_128; lean_object* x_129; lean_object* x_130; lean_object* x_131; lean_object* x_132; lean_object* x_133; lean_object* x_134; 
-x_98 = lean_ctor_get(x_34, 0);
-x_99 = lean_ctor_get(x_34, 2);
-x_100 = lean_ctor_get(x_34, 3);
-x_101 = lean_ctor_get(x_34, 4);
-lean_inc(x_101);
-lean_inc(x_100);
-lean_inc(x_99);
-lean_inc(x_98);
-lean_dec(x_34);
-x_102 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__5;
-x_103 = lean_alloc_ctor(0, 5, 0);
-lean_ctor_set(x_103, 0, x_98);
-lean_ctor_set(x_103, 1, x_102);
-lean_ctor_set(x_103, 2, x_99);
-lean_ctor_set(x_103, 3, x_100);
-lean_ctor_set(x_103, 4, x_101);
-x_104 = lean_st_ref_set(x_3, x_103, x_35);
-x_105 = lean_ctor_get(x_104, 1);
-lean_inc(x_105);
-lean_dec(x_104);
-x_106 = lean_st_ref_take(x_5, x_105);
-x_107 = lean_ctor_get(x_106, 0);
-lean_inc(x_107);
-x_108 = lean_ctor_get(x_106, 1);
-lean_inc(x_108);
-lean_dec(x_106);
-x_109 = lean_ctor_get(x_107, 0);
-lean_inc(x_109);
-x_110 = lean_ctor_get(x_107, 1);
-lean_inc(x_110);
-x_111 = lean_ctor_get(x_107, 2);
-lean_inc(x_111);
-x_112 = lean_ctor_get(x_107, 3);
-lean_inc(x_112);
-x_113 = lean_ctor_get(x_107, 5);
-lean_inc(x_113);
-x_114 = lean_ctor_get(x_107, 6);
-lean_inc(x_114);
-if (lean_is_exclusive(x_107)) {
- lean_ctor_release(x_107, 0);
- lean_ctor_release(x_107, 1);
- lean_ctor_release(x_107, 2);
- lean_ctor_release(x_107, 3);
- lean_ctor_release(x_107, 4);
- lean_ctor_release(x_107, 5);
- lean_ctor_release(x_107, 6);
- x_115 = x_107;
-} else {
- lean_dec_ref(x_107);
- x_115 = lean_box(0);
-}
-x_116 = l_Lean_mkRecOn___closed__2;
-x_117 = l_Lean_TagDeclarationExtension_tag(x_116, x_109, x_8);
-if (lean_is_scalar(x_115)) {
- x_118 = lean_alloc_ctor(0, 7, 0);
-} else {
- x_118 = x_115;
-}
-lean_ctor_set(x_118, 0, x_117);
-lean_ctor_set(x_118, 1, x_110);
-lean_ctor_set(x_118, 2, x_111);
-lean_ctor_set(x_118, 3, x_112);
-lean_ctor_set(x_118, 4, x_30);
-lean_ctor_set(x_118, 5, x_113);
-lean_ctor_set(x_118, 6, x_114);
-x_119 = lean_st_ref_set(x_5, x_118, x_108);
-lean_dec(x_5);
-x_120 = lean_ctor_get(x_119, 1);
-lean_inc(x_120);
-lean_dec(x_119);
-x_121 = lean_st_ref_take(x_3, x_120);
-x_122 = lean_ctor_get(x_121, 0);
-lean_inc(x_122);
-x_123 = lean_ctor_get(x_121, 1);
-lean_inc(x_123);
-lean_dec(x_121);
-x_124 = lean_ctor_get(x_122, 0);
-lean_inc(x_124);
-x_125 = lean_ctor_get(x_122, 2);
-lean_inc(x_125);
-x_126 = lean_ctor_get(x_122, 3);
-lean_inc(x_126);
-x_127 = lean_ctor_get(x_122, 4);
-lean_inc(x_127);
-if (lean_is_exclusive(x_122)) {
- lean_ctor_release(x_122, 0);
- lean_ctor_release(x_122, 1);
- lean_ctor_release(x_122, 2);
- lean_ctor_release(x_122, 3);
- lean_ctor_release(x_122, 4);
- x_128 = x_122;
-} else {
- lean_dec_ref(x_122);
- x_128 = lean_box(0);
-}
-if (lean_is_scalar(x_128)) {
- x_129 = lean_alloc_ctor(0, 5, 0);
-} else {
- x_129 = x_128;
-}
-lean_ctor_set(x_129, 0, x_124);
-lean_ctor_set(x_129, 1, x_102);
-lean_ctor_set(x_129, 2, x_125);
-lean_ctor_set(x_129, 3, x_126);
-lean_ctor_set(x_129, 4, x_127);
-x_130 = lean_st_ref_set(x_3, x_129, x_123);
-x_131 = lean_ctor_get(x_130, 1);
-lean_inc(x_131);
-if (lean_is_exclusive(x_130)) {
- lean_ctor_release(x_130, 0);
- lean_ctor_release(x_130, 1);
- x_132 = x_130;
-} else {
- lean_dec_ref(x_130);
- x_132 = lean_box(0);
-}
-x_133 = lean_box(0);
-if (lean_is_scalar(x_132)) {
- x_134 = lean_alloc_ctor(0, 2, 0);
-} else {
- x_134 = x_132;
-}
-lean_ctor_set(x_134, 0, x_133);
-lean_ctor_set(x_134, 1, x_131);
-return x_134;
-}
-}
-else
-{
-lean_object* x_135; lean_object* x_136; lean_object* x_137; lean_object* x_138; lean_object* x_139; lean_object* x_140; lean_object* x_141; lean_object* x_142; lean_object* x_143; lean_object* x_144; lean_object* x_145; lean_object* x_146; lean_object* x_147; lean_object* x_148; lean_object* x_149; lean_object* x_150; lean_object* x_151; lean_object* x_152; lean_object* x_153; lean_object* x_154; lean_object* x_155; lean_object* x_156; lean_object* x_157; lean_object* x_158; lean_object* x_159; lean_object* x_160; lean_object* x_161; lean_object* x_162; lean_object* x_163; lean_object* x_164; lean_object* x_165; lean_object* x_166; lean_object* x_167; lean_object* x_168; lean_object* x_169; lean_object* x_170; lean_object* x_171; lean_object* x_172; lean_object* x_173; lean_object* x_174; lean_object* x_175; lean_object* x_176; lean_object* x_177; lean_object* x_178; lean_object* x_179; lean_object* x_180; lean_object* x_181; lean_object* x_182; lean_object* x_183; lean_object* x_184; lean_object* x_185; lean_object* x_186; lean_object* x_187; 
-x_135 = lean_ctor_get(x_23, 0);
-x_136 = lean_ctor_get(x_23, 1);
-x_137 = lean_ctor_get(x_23, 2);
-x_138 = lean_ctor_get(x_23, 3);
-x_139 = lean_ctor_get(x_23, 5);
-x_140 = lean_ctor_get(x_23, 6);
-lean_inc(x_140);
-lean_inc(x_139);
-lean_inc(x_138);
-lean_inc(x_137);
-lean_inc(x_136);
-lean_inc(x_135);
-lean_dec(x_23);
-x_141 = l_Lean_mkRecOn___closed__1;
-lean_inc(x_8);
-x_142 = l_Lean_TagDeclarationExtension_tag(x_141, x_135, x_8);
-x_143 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__3;
-x_144 = lean_alloc_ctor(0, 7, 0);
-lean_ctor_set(x_144, 0, x_142);
-lean_ctor_set(x_144, 1, x_136);
-lean_ctor_set(x_144, 2, x_137);
-lean_ctor_set(x_144, 3, x_138);
-lean_ctor_set(x_144, 4, x_143);
-lean_ctor_set(x_144, 5, x_139);
-lean_ctor_set(x_144, 6, x_140);
-x_145 = lean_st_ref_set(x_5, x_144, x_24);
-x_146 = lean_ctor_get(x_145, 1);
-lean_inc(x_146);
-lean_dec(x_145);
-x_147 = lean_st_ref_take(x_3, x_146);
-x_148 = lean_ctor_get(x_147, 0);
-lean_inc(x_148);
-x_149 = lean_ctor_get(x_147, 1);
-lean_inc(x_149);
-lean_dec(x_147);
-x_150 = lean_ctor_get(x_148, 0);
-lean_inc(x_150);
-x_151 = lean_ctor_get(x_148, 2);
-lean_inc(x_151);
-x_152 = lean_ctor_get(x_148, 3);
-lean_inc(x_152);
-x_153 = lean_ctor_get(x_148, 4);
-lean_inc(x_153);
-if (lean_is_exclusive(x_148)) {
- lean_ctor_release(x_148, 0);
- lean_ctor_release(x_148, 1);
- lean_ctor_release(x_148, 2);
- lean_ctor_release(x_148, 3);
- lean_ctor_release(x_148, 4);
- x_154 = x_148;
-} else {
- lean_dec_ref(x_148);
- x_154 = lean_box(0);
-}
-x_155 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__5;
-if (lean_is_scalar(x_154)) {
- x_156 = lean_alloc_ctor(0, 5, 0);
-} else {
- x_156 = x_154;
-}
-lean_ctor_set(x_156, 0, x_150);
-lean_ctor_set(x_156, 1, x_155);
-lean_ctor_set(x_156, 2, x_151);
-lean_ctor_set(x_156, 3, x_152);
-lean_ctor_set(x_156, 4, x_153);
-x_157 = lean_st_ref_set(x_3, x_156, x_149);
-x_158 = lean_ctor_get(x_157, 1);
-lean_inc(x_158);
-lean_dec(x_157);
-x_159 = lean_st_ref_take(x_5, x_158);
-x_160 = lean_ctor_get(x_159, 0);
-lean_inc(x_160);
-x_161 = lean_ctor_get(x_159, 1);
-lean_inc(x_161);
-lean_dec(x_159);
-x_162 = lean_ctor_get(x_160, 0);
-lean_inc(x_162);
-x_163 = lean_ctor_get(x_160, 1);
-lean_inc(x_163);
-x_164 = lean_ctor_get(x_160, 2);
-lean_inc(x_164);
-x_165 = lean_ctor_get(x_160, 3);
-lean_inc(x_165);
-x_166 = lean_ctor_get(x_160, 5);
-lean_inc(x_166);
-x_167 = lean_ctor_get(x_160, 6);
-lean_inc(x_167);
-if (lean_is_exclusive(x_160)) {
- lean_ctor_release(x_160, 0);
- lean_ctor_release(x_160, 1);
- lean_ctor_release(x_160, 2);
- lean_ctor_release(x_160, 3);
- lean_ctor_release(x_160, 4);
- lean_ctor_release(x_160, 5);
- lean_ctor_release(x_160, 6);
- x_168 = x_160;
-} else {
- lean_dec_ref(x_160);
- x_168 = lean_box(0);
-}
-x_169 = l_Lean_mkRecOn___closed__2;
-x_170 = l_Lean_TagDeclarationExtension_tag(x_169, x_162, x_8);
-if (lean_is_scalar(x_168)) {
- x_171 = lean_alloc_ctor(0, 7, 0);
-} else {
- x_171 = x_168;
-}
-lean_ctor_set(x_171, 0, x_170);
-lean_ctor_set(x_171, 1, x_163);
-lean_ctor_set(x_171, 2, x_164);
-lean_ctor_set(x_171, 3, x_165);
-lean_ctor_set(x_171, 4, x_143);
-lean_ctor_set(x_171, 5, x_166);
-lean_ctor_set(x_171, 6, x_167);
-x_172 = lean_st_ref_set(x_5, x_171, x_161);
-lean_dec(x_5);
-x_173 = lean_ctor_get(x_172, 1);
-lean_inc(x_173);
-lean_dec(x_172);
-x_174 = lean_st_ref_take(x_3, x_173);
-x_175 = lean_ctor_get(x_174, 0);
-lean_inc(x_175);
-x_176 = lean_ctor_get(x_174, 1);
-lean_inc(x_176);
-lean_dec(x_174);
-x_177 = lean_ctor_get(x_175, 0);
-lean_inc(x_177);
-x_178 = lean_ctor_get(x_175, 2);
-lean_inc(x_178);
-x_179 = lean_ctor_get(x_175, 3);
-lean_inc(x_179);
-x_180 = lean_ctor_get(x_175, 4);
-lean_inc(x_180);
-if (lean_is_exclusive(x_175)) {
- lean_ctor_release(x_175, 0);
- lean_ctor_release(x_175, 1);
- lean_ctor_release(x_175, 2);
- lean_ctor_release(x_175, 3);
- lean_ctor_release(x_175, 4);
- x_181 = x_175;
-} else {
- lean_dec_ref(x_175);
- x_181 = lean_box(0);
-}
-if (lean_is_scalar(x_181)) {
- x_182 = lean_alloc_ctor(0, 5, 0);
-} else {
- x_182 = x_181;
-}
-lean_ctor_set(x_182, 0, x_177);
-lean_ctor_set(x_182, 1, x_155);
-lean_ctor_set(x_182, 2, x_178);
-lean_ctor_set(x_182, 3, x_179);
-lean_ctor_set(x_182, 4, x_180);
-x_183 = lean_st_ref_set(x_3, x_182, x_176);
-x_184 = lean_ctor_get(x_183, 1);
-lean_inc(x_184);
-if (lean_is_exclusive(x_183)) {
- lean_ctor_release(x_183, 0);
- lean_ctor_release(x_183, 1);
- x_185 = x_183;
-} else {
- lean_dec_ref(x_183);
- x_185 = lean_box(0);
-}
-x_186 = lean_box(0);
-if (lean_is_scalar(x_185)) {
- x_187 = lean_alloc_ctor(0, 2, 0);
-} else {
- x_187 = x_185;
-}
-lean_ctor_set(x_187, 0, x_186);
-lean_ctor_set(x_187, 1, x_184);
-return x_187;
-}
-}
-else
-{
-uint8_t x_188; 
-lean_dec(x_8);
-lean_dec(x_5);
-lean_dec(x_4);
-x_188 = !lean_is_exclusive(x_17);
-if (x_188 == 0)
-{
-return x_17;
-}
-else
-{
-lean_object* x_189; lean_object* x_190; lean_object* x_191; 
-x_189 = lean_ctor_get(x_17, 0);
-x_190 = lean_ctor_get(x_17, 1);
-lean_inc(x_190);
-lean_inc(x_189);
-lean_dec(x_17);
-x_191 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_191, 0, x_189);
-lean_ctor_set(x_191, 1, x_190);
-return x_191;
-}
-}
-}
-else
-{
-uint8_t x_192; 
-lean_dec(x_8);
-lean_dec(x_5);
-lean_dec(x_4);
-x_192 = !lean_is_exclusive(x_14);
-if (x_192 == 0)
-{
-return x_14;
-}
-else
-{
-lean_object* x_193; lean_object* x_194; lean_object* x_195; 
-x_193 = lean_ctor_get(x_14, 0);
-x_194 = lean_ctor_get(x_14, 1);
-lean_inc(x_194);
-lean_inc(x_193);
-lean_dec(x_14);
-x_195 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_195, 0, x_193);
-lean_ctor_set(x_195, 1, x_194);
-return x_195;
-}
-}
-}
-}
-LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_mkRecOn___spec__3___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
-_start:
-{
-lean_object* x_7; 
-x_7 = l_Lean_throwError___at_Lean_mkRecOn___spec__3(x_1, x_2, x_3, x_4, x_5, x_6);
-lean_dec(x_5);
-lean_dec(x_4);
-lean_dec(x_3);
-lean_dec(x_2);
-return x_7;
-}
-}
-LEAN_EXPORT lean_object* l_Lean_throwKernelException___at_Lean_mkRecOn___spec__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
-_start:
-{
-lean_object* x_7; 
-x_7 = l_Lean_throwKernelException___at_Lean_mkRecOn___spec__2(x_1, x_2, x_3, x_4, x_5, x_6);
-lean_dec(x_5);
-lean_dec(x_3);
-lean_dec(x_2);
-return x_7;
-}
-}
-LEAN_EXPORT lean_object* l_Lean_ofExceptKernelException___at_Lean_mkRecOn___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
-_start:
-{
-lean_object* x_7; 
-x_7 = l_Lean_ofExceptKernelException___at_Lean_mkRecOn___spec__1(x_1, x_2, x_3, x_4, x_5, x_6);
-lean_dec(x_5);
-lean_dec(x_3);
-lean_dec(x_2);
-return x_7;
-}
-}
-LEAN_EXPORT lean_object* l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
-_start:
-{
-uint8_t x_8; lean_object* x_9; 
-x_8 = lean_unbox(x_2);
-lean_dec(x_2);
-x_9 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4(x_1, x_8, x_3, x_4, x_5, x_6, x_7);
-lean_dec(x_6);
-lean_dec(x_5);
-lean_dec(x_4);
-lean_dec(x_3);
-return x_9;
-}
-}
-LEAN_EXPORT lean_object* l_Lean_mkRecOn___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
-_start:
-{
-lean_object* x_7; 
-x_7 = l_Lean_mkRecOn(x_1, x_2, x_3, x_4, x_5, x_6);
-lean_dec(x_3);
-lean_dec(x_2);
-return x_7;
-}
-}
 LEAN_EXPORT lean_object* l_Lean_mkCasesOn(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
 _start:
 {
@@ -1297,7 +392,7 @@ lean_dec(x_10);
 x_13 = lean_mk_cases_on(x_12, x_1);
 lean_dec(x_1);
 lean_inc(x_4);
-x_14 = l_Lean_ofExceptKernelException___at_Lean_mkRecOn___spec__1(x_13, x_2, x_3, x_4, x_5, x_11);
+x_14 = l_Lean_ofExceptKernelException___at_Lean_mkCasesOn___spec__1(x_13, x_2, x_3, x_4, x_5, x_11);
 if (lean_obj_tag(x_14) == 0)
 {
 lean_object* x_15; lean_object* x_16; lean_object* x_17; 
@@ -1317,7 +412,7 @@ lean_inc(x_18);
 lean_dec(x_17);
 x_19 = 0;
 lean_inc(x_8);
-x_20 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4(x_8, x_19, x_2, x_3, x_4, x_5, x_18);
+x_20 = l_Lean_setReducibilityStatus___at_mkRecOn___spec__3(x_8, x_19, x_2, x_3, x_4, x_5, x_18);
 lean_dec(x_4);
 x_21 = lean_ctor_get(x_20, 1);
 lean_inc(x_21);
@@ -1335,10 +430,10 @@ lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean
 x_26 = lean_ctor_get(x_23, 0);
 x_27 = lean_ctor_get(x_23, 4);
 lean_dec(x_27);
-x_28 = l_Lean_mkRecOn___closed__1;
+x_28 = l_Lean_mkCasesOn___closed__1;
 lean_inc(x_8);
 x_29 = l_Lean_TagDeclarationExtension_tag(x_28, x_26, x_8);
-x_30 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__3;
+x_30 = l_Lean_mkCasesOn___closed__4;
 lean_ctor_set(x_23, 4, x_30);
 lean_ctor_set(x_23, 0, x_29);
 x_31 = lean_st_ref_set(x_5, x_23, x_24);
@@ -1357,7 +452,7 @@ if (x_36 == 0)
 lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; uint8_t x_44; 
 x_37 = lean_ctor_get(x_34, 1);
 lean_dec(x_37);
-x_38 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__5;
+x_38 = l_Lean_mkCasesOn___closed__6;
 lean_ctor_set(x_34, 1, x_38);
 x_39 = lean_st_ref_set(x_3, x_34, x_35);
 x_40 = lean_ctor_get(x_39, 1);
@@ -1376,7 +471,7 @@ lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean
 x_45 = lean_ctor_get(x_42, 0);
 x_46 = lean_ctor_get(x_42, 4);
 lean_dec(x_46);
-x_47 = l_Lean_mkRecOn___closed__2;
+x_47 = l_Lean_mkCasesOn___closed__7;
 x_48 = l_Lean_TagDeclarationExtension_tag(x_47, x_45, x_8);
 lean_ctor_set(x_42, 4, x_30);
 lean_ctor_set(x_42, 0, x_48);
@@ -1478,7 +573,7 @@ lean_inc(x_75);
 lean_inc(x_74);
 lean_inc(x_73);
 lean_dec(x_42);
-x_79 = l_Lean_mkRecOn___closed__2;
+x_79 = l_Lean_mkCasesOn___closed__7;
 x_80 = l_Lean_TagDeclarationExtension_tag(x_79, x_73, x_8);
 x_81 = lean_alloc_ctor(0, 7, 0);
 lean_ctor_set(x_81, 0, x_80);
@@ -1562,7 +657,7 @@ lean_inc(x_100);
 lean_inc(x_99);
 lean_inc(x_98);
 lean_dec(x_34);
-x_102 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__5;
+x_102 = l_Lean_mkCasesOn___closed__6;
 x_103 = lean_alloc_ctor(0, 5, 0);
 lean_ctor_set(x_103, 0, x_98);
 lean_ctor_set(x_103, 1, x_102);
@@ -1604,7 +699,7 @@ if (lean_is_exclusive(x_107)) {
  lean_dec_ref(x_107);
  x_115 = lean_box(0);
 }
-x_116 = l_Lean_mkRecOn___closed__2;
+x_116 = l_Lean_mkCasesOn___closed__7;
 x_117 = l_Lean_TagDeclarationExtension_tag(x_116, x_109, x_8);
 if (lean_is_scalar(x_115)) {
  x_118 = lean_alloc_ctor(0, 7, 0);
@@ -1696,10 +791,10 @@ lean_inc(x_137);
 lean_inc(x_136);
 lean_inc(x_135);
 lean_dec(x_23);
-x_141 = l_Lean_mkRecOn___closed__1;
+x_141 = l_Lean_mkCasesOn___closed__1;
 lean_inc(x_8);
 x_142 = l_Lean_TagDeclarationExtension_tag(x_141, x_135, x_8);
-x_143 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__3;
+x_143 = l_Lean_mkCasesOn___closed__4;
 x_144 = lean_alloc_ctor(0, 7, 0);
 lean_ctor_set(x_144, 0, x_142);
 lean_ctor_set(x_144, 1, x_136);
@@ -1737,7 +832,7 @@ if (lean_is_exclusive(x_148)) {
  lean_dec_ref(x_148);
  x_154 = lean_box(0);
 }
-x_155 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__5;
+x_155 = l_Lean_mkCasesOn___closed__6;
 if (lean_is_scalar(x_154)) {
  x_156 = lean_alloc_ctor(0, 5, 0);
 } else {
@@ -1783,7 +878,7 @@ if (lean_is_exclusive(x_160)) {
  lean_dec_ref(x_160);
  x_168 = lean_box(0);
 }
-x_169 = l_Lean_mkRecOn___closed__2;
+x_169 = l_Lean_mkCasesOn___closed__7;
 x_170 = l_Lean_TagDeclarationExtension_tag(x_169, x_162, x_8);
 if (lean_is_scalar(x_168)) {
  x_171 = lean_alloc_ctor(0, 7, 0);
@@ -1912,6 +1007,40 @@ return x_195;
 }
 }
 }
+LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_mkCasesOn___spec__3___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
+_start:
+{
+lean_object* x_7; 
+x_7 = l_Lean_throwError___at_Lean_mkCasesOn___spec__3(x_1, x_2, x_3, x_4, x_5, x_6);
+lean_dec(x_5);
+lean_dec(x_4);
+lean_dec(x_3);
+lean_dec(x_2);
+return x_7;
+}
+}
+LEAN_EXPORT lean_object* l_Lean_throwKernelException___at_Lean_mkCasesOn___spec__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
+_start:
+{
+lean_object* x_7; 
+x_7 = l_Lean_throwKernelException___at_Lean_mkCasesOn___spec__2(x_1, x_2, x_3, x_4, x_5, x_6);
+lean_dec(x_5);
+lean_dec(x_3);
+lean_dec(x_2);
+return x_7;
+}
+}
+LEAN_EXPORT lean_object* l_Lean_ofExceptKernelException___at_Lean_mkCasesOn___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
+_start:
+{
+lean_object* x_7; 
+x_7 = l_Lean_ofExceptKernelException___at_Lean_mkCasesOn___spec__1(x_1, x_2, x_3, x_4, x_5, x_6);
+lean_dec(x_5);
+lean_dec(x_3);
+lean_dec(x_2);
+return x_7;
+}
+}
 LEAN_EXPORT lean_object* l_Lean_mkCasesOn___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
 _start:
 {
@@ -1945,7 +1074,7 @@ lean_inc(x_12);
 lean_dec(x_10);
 x_13 = lean_mk_below(x_12, x_1, x_2);
 lean_inc(x_6);
-x_14 = l_Lean_ofExceptKernelException___at_Lean_mkRecOn___spec__1(x_13, x_4, x_5, x_6, x_7, x_11);
+x_14 = l_Lean_ofExceptKernelException___at_Lean_mkCasesOn___spec__1(x_13, x_4, x_5, x_6, x_7, x_11);
 if (lean_obj_tag(x_14) == 0)
 {
 lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; 
@@ -1972,7 +1101,7 @@ lean_inc(x_21);
 lean_dec(x_20);
 x_22 = 0;
 lean_inc(x_19);
-x_23 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4(x_19, x_22, x_4, x_5, x_6, x_7, x_21);
+x_23 = l_Lean_setReducibilityStatus___at_mkRecOn___spec__3(x_19, x_22, x_4, x_5, x_6, x_7, x_21);
 lean_dec(x_6);
 x_24 = lean_ctor_get(x_23, 1);
 lean_inc(x_24);
@@ -1993,7 +1122,7 @@ lean_dec(x_30);
 x_31 = l___private_Lean_Meta_Constructions_0__Lean_mkBelowOrIBelow___lambda__1___closed__1;
 lean_inc(x_19);
 x_32 = l_Lean_TagDeclarationExtension_tag(x_31, x_29, x_19);
-x_33 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__3;
+x_33 = l_Lean_mkCasesOn___closed__4;
 lean_ctor_set(x_26, 4, x_33);
 lean_ctor_set(x_26, 0, x_32);
 x_34 = lean_st_ref_set(x_7, x_26, x_27);
@@ -2012,7 +1141,7 @@ if (x_39 == 0)
 lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; uint8_t x_47; 
 x_40 = lean_ctor_get(x_37, 1);
 lean_dec(x_40);
-x_41 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__5;
+x_41 = l_Lean_mkCasesOn___closed__6;
 lean_ctor_set(x_37, 1, x_41);
 x_42 = lean_st_ref_set(x_5, x_37, x_38);
 x_43 = lean_ctor_get(x_42, 1);
@@ -2031,7 +1160,7 @@ lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean
 x_48 = lean_ctor_get(x_45, 0);
 x_49 = lean_ctor_get(x_45, 4);
 lean_dec(x_49);
-x_50 = l_Lean_mkRecOn___closed__2;
+x_50 = l_Lean_mkCasesOn___closed__7;
 x_51 = l_Lean_TagDeclarationExtension_tag(x_50, x_48, x_19);
 lean_ctor_set(x_45, 4, x_33);
 lean_ctor_set(x_45, 0, x_51);
@@ -2133,7 +1262,7 @@ lean_inc(x_78);
 lean_inc(x_77);
 lean_inc(x_76);
 lean_dec(x_45);
-x_82 = l_Lean_mkRecOn___closed__2;
+x_82 = l_Lean_mkCasesOn___closed__7;
 x_83 = l_Lean_TagDeclarationExtension_tag(x_82, x_76, x_19);
 x_84 = lean_alloc_ctor(0, 7, 0);
 lean_ctor_set(x_84, 0, x_83);
@@ -2217,7 +1346,7 @@ lean_inc(x_103);
 lean_inc(x_102);
 lean_inc(x_101);
 lean_dec(x_37);
-x_105 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__5;
+x_105 = l_Lean_mkCasesOn___closed__6;
 x_106 = lean_alloc_ctor(0, 5, 0);
 lean_ctor_set(x_106, 0, x_101);
 lean_ctor_set(x_106, 1, x_105);
@@ -2259,7 +1388,7 @@ if (lean_is_exclusive(x_110)) {
  lean_dec_ref(x_110);
  x_118 = lean_box(0);
 }
-x_119 = l_Lean_mkRecOn___closed__2;
+x_119 = l_Lean_mkCasesOn___closed__7;
 x_120 = l_Lean_TagDeclarationExtension_tag(x_119, x_112, x_19);
 if (lean_is_scalar(x_118)) {
  x_121 = lean_alloc_ctor(0, 7, 0);
@@ -2354,7 +1483,7 @@ lean_dec(x_26);
 x_144 = l___private_Lean_Meta_Constructions_0__Lean_mkBelowOrIBelow___lambda__1___closed__1;
 lean_inc(x_19);
 x_145 = l_Lean_TagDeclarationExtension_tag(x_144, x_138, x_19);
-x_146 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__3;
+x_146 = l_Lean_mkCasesOn___closed__4;
 x_147 = lean_alloc_ctor(0, 7, 0);
 lean_ctor_set(x_147, 0, x_145);
 lean_ctor_set(x_147, 1, x_139);
@@ -2392,7 +1521,7 @@ if (lean_is_exclusive(x_151)) {
  lean_dec_ref(x_151);
  x_157 = lean_box(0);
 }
-x_158 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__5;
+x_158 = l_Lean_mkCasesOn___closed__6;
 if (lean_is_scalar(x_157)) {
  x_159 = lean_alloc_ctor(0, 5, 0);
 } else {
@@ -2438,7 +1567,7 @@ if (lean_is_exclusive(x_163)) {
  lean_dec_ref(x_163);
  x_171 = lean_box(0);
 }
-x_172 = l_Lean_mkRecOn___closed__2;
+x_172 = l_Lean_mkCasesOn___closed__7;
 x_173 = l_Lean_TagDeclarationExtension_tag(x_172, x_165, x_19);
 if (lean_is_scalar(x_171)) {
  x_174 = lean_alloc_ctor(0, 7, 0);
@@ -2852,7 +1981,7 @@ lean_inc(x_12);
 lean_dec(x_10);
 x_13 = lean_mk_brec_on(x_12, x_1, x_2);
 lean_inc(x_6);
-x_14 = l_Lean_ofExceptKernelException___at_Lean_mkRecOn___spec__1(x_13, x_4, x_5, x_6, x_7, x_11);
+x_14 = l_Lean_ofExceptKernelException___at_Lean_mkCasesOn___spec__1(x_13, x_4, x_5, x_6, x_7, x_11);
 if (lean_obj_tag(x_14) == 0)
 {
 lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; 
@@ -2879,7 +2008,7 @@ lean_inc(x_21);
 lean_dec(x_20);
 x_22 = 0;
 lean_inc(x_19);
-x_23 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4(x_19, x_22, x_4, x_5, x_6, x_7, x_21);
+x_23 = l_Lean_setReducibilityStatus___at_mkRecOn___spec__3(x_19, x_22, x_4, x_5, x_6, x_7, x_21);
 lean_dec(x_6);
 x_24 = lean_ctor_get(x_23, 1);
 lean_inc(x_24);
@@ -2897,10 +2026,10 @@ lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean
 x_29 = lean_ctor_get(x_26, 0);
 x_30 = lean_ctor_get(x_26, 4);
 lean_dec(x_30);
-x_31 = l_Lean_mkRecOn___closed__1;
+x_31 = l_Lean_mkCasesOn___closed__1;
 lean_inc(x_19);
 x_32 = l_Lean_TagDeclarationExtension_tag(x_31, x_29, x_19);
-x_33 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__3;
+x_33 = l_Lean_mkCasesOn___closed__4;
 lean_ctor_set(x_26, 4, x_33);
 lean_ctor_set(x_26, 0, x_32);
 x_34 = lean_st_ref_set(x_7, x_26, x_27);
@@ -2919,7 +2048,7 @@ if (x_39 == 0)
 lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; uint8_t x_47; 
 x_40 = lean_ctor_get(x_37, 1);
 lean_dec(x_40);
-x_41 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__5;
+x_41 = l_Lean_mkCasesOn___closed__6;
 lean_ctor_set(x_37, 1, x_41);
 x_42 = lean_st_ref_set(x_5, x_37, x_38);
 x_43 = lean_ctor_get(x_42, 1);
@@ -2938,7 +2067,7 @@ lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean
 x_48 = lean_ctor_get(x_45, 0);
 x_49 = lean_ctor_get(x_45, 4);
 lean_dec(x_49);
-x_50 = l_Lean_mkRecOn___closed__2;
+x_50 = l_Lean_mkCasesOn___closed__7;
 x_51 = l_Lean_TagDeclarationExtension_tag(x_50, x_48, x_19);
 lean_ctor_set(x_45, 4, x_33);
 lean_ctor_set(x_45, 0, x_51);
@@ -3040,7 +2169,7 @@ lean_inc(x_78);
 lean_inc(x_77);
 lean_inc(x_76);
 lean_dec(x_45);
-x_82 = l_Lean_mkRecOn___closed__2;
+x_82 = l_Lean_mkCasesOn___closed__7;
 x_83 = l_Lean_TagDeclarationExtension_tag(x_82, x_76, x_19);
 x_84 = lean_alloc_ctor(0, 7, 0);
 lean_ctor_set(x_84, 0, x_83);
@@ -3124,7 +2253,7 @@ lean_inc(x_103);
 lean_inc(x_102);
 lean_inc(x_101);
 lean_dec(x_37);
-x_105 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__5;
+x_105 = l_Lean_mkCasesOn___closed__6;
 x_106 = lean_alloc_ctor(0, 5, 0);
 lean_ctor_set(x_106, 0, x_101);
 lean_ctor_set(x_106, 1, x_105);
@@ -3166,7 +2295,7 @@ if (lean_is_exclusive(x_110)) {
  lean_dec_ref(x_110);
  x_118 = lean_box(0);
 }
-x_119 = l_Lean_mkRecOn___closed__2;
+x_119 = l_Lean_mkCasesOn___closed__7;
 x_120 = l_Lean_TagDeclarationExtension_tag(x_119, x_112, x_19);
 if (lean_is_scalar(x_118)) {
  x_121 = lean_alloc_ctor(0, 7, 0);
@@ -3258,10 +2387,10 @@ lean_inc(x_140);
 lean_inc(x_139);
 lean_inc(x_138);
 lean_dec(x_26);
-x_144 = l_Lean_mkRecOn___closed__1;
+x_144 = l_Lean_mkCasesOn___closed__1;
 lean_inc(x_19);
 x_145 = l_Lean_TagDeclarationExtension_tag(x_144, x_138, x_19);
-x_146 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__3;
+x_146 = l_Lean_mkCasesOn___closed__4;
 x_147 = lean_alloc_ctor(0, 7, 0);
 lean_ctor_set(x_147, 0, x_145);
 lean_ctor_set(x_147, 1, x_139);
@@ -3299,7 +2428,7 @@ if (lean_is_exclusive(x_151)) {
  lean_dec_ref(x_151);
  x_157 = lean_box(0);
 }
-x_158 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__5;
+x_158 = l_Lean_mkCasesOn___closed__6;
 if (lean_is_scalar(x_157)) {
  x_159 = lean_alloc_ctor(0, 5, 0);
 } else {
@@ -3345,7 +2474,7 @@ if (lean_is_exclusive(x_163)) {
  lean_dec_ref(x_163);
  x_171 = lean_box(0);
 }
-x_172 = l_Lean_mkRecOn___closed__2;
+x_172 = l_Lean_mkCasesOn___closed__7;
 x_173 = l_Lean_TagDeclarationExtension_tag(x_172, x_165, x_19);
 if (lean_is_scalar(x_171)) {
  x_174 = lean_alloc_ctor(0, 7, 0);
@@ -3961,7 +3090,7 @@ lean_inc(x_13);
 lean_dec(x_11);
 x_14 = lean_mk_no_confusion_type(x_13, x_1);
 lean_inc(x_5);
-x_15 = l_Lean_ofExceptKernelException___at_Lean_mkRecOn___spec__1(x_14, x_3, x_4, x_5, x_6, x_12);
+x_15 = l_Lean_ofExceptKernelException___at_Lean_mkCasesOn___spec__1(x_14, x_3, x_4, x_5, x_6, x_12);
 if (lean_obj_tag(x_15) == 0)
 {
 lean_object* x_16; lean_object* x_17; lean_object* x_18; 
@@ -3981,7 +3110,7 @@ lean_inc(x_19);
 lean_dec(x_18);
 x_20 = 0;
 lean_inc(x_9);
-x_21 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4(x_9, x_20, x_3, x_4, x_5, x_6, x_19);
+x_21 = l_Lean_setReducibilityStatus___at_mkRecOn___spec__3(x_9, x_20, x_3, x_4, x_5, x_6, x_19);
 x_22 = lean_ctor_get(x_21, 1);
 lean_inc(x_22);
 lean_dec(x_21);
@@ -4001,7 +3130,7 @@ lean_dec(x_28);
 x_29 = l___private_Lean_Meta_Constructions_0__Lean_mkBelowOrIBelow___lambda__1___closed__1;
 lean_inc(x_9);
 x_30 = l_Lean_TagDeclarationExtension_tag(x_29, x_27, x_9);
-x_31 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__3;
+x_31 = l_Lean_mkCasesOn___closed__4;
 lean_ctor_set(x_24, 4, x_31);
 lean_ctor_set(x_24, 0, x_30);
 x_32 = lean_st_ref_set(x_6, x_24, x_25);
@@ -4020,7 +3149,7 @@ if (x_37 == 0)
 lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; uint8_t x_45; 
 x_38 = lean_ctor_get(x_35, 1);
 lean_dec(x_38);
-x_39 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__5;
+x_39 = l_Lean_mkCasesOn___closed__6;
 lean_ctor_set(x_35, 1, x_39);
 x_40 = lean_st_ref_set(x_4, x_35, x_36);
 x_41 = lean_ctor_get(x_40, 1);
@@ -4039,7 +3168,7 @@ lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean
 x_46 = lean_ctor_get(x_43, 0);
 x_47 = lean_ctor_get(x_43, 4);
 lean_dec(x_47);
-x_48 = l_Lean_mkRecOn___closed__2;
+x_48 = l_Lean_mkCasesOn___closed__7;
 x_49 = l_Lean_TagDeclarationExtension_tag(x_48, x_46, x_9);
 lean_ctor_set(x_43, 4, x_31);
 lean_ctor_set(x_43, 0, x_49);
@@ -4079,7 +3208,7 @@ lean_dec(x_62);
 x_65 = lean_mk_no_confusion(x_64, x_1);
 lean_dec(x_1);
 lean_inc(x_5);
-x_66 = l_Lean_ofExceptKernelException___at_Lean_mkRecOn___spec__1(x_65, x_3, x_4, x_5, x_6, x_63);
+x_66 = l_Lean_ofExceptKernelException___at_Lean_mkCasesOn___spec__1(x_65, x_3, x_4, x_5, x_6, x_63);
 if (lean_obj_tag(x_66) == 0)
 {
 lean_object* x_67; lean_object* x_68; lean_object* x_69; 
@@ -4098,7 +3227,7 @@ x_70 = lean_ctor_get(x_69, 1);
 lean_inc(x_70);
 lean_dec(x_69);
 lean_inc(x_60);
-x_71 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4(x_60, x_20, x_3, x_4, x_5, x_6, x_70);
+x_71 = l_Lean_setReducibilityStatus___at_mkRecOn___spec__3(x_60, x_20, x_3, x_4, x_5, x_6, x_70);
 lean_dec(x_5);
 x_72 = lean_ctor_get(x_71, 1);
 lean_inc(x_72);
@@ -4720,7 +3849,7 @@ lean_dec(x_248);
 x_251 = lean_mk_no_confusion(x_250, x_1);
 lean_dec(x_1);
 lean_inc(x_5);
-x_252 = l_Lean_ofExceptKernelException___at_Lean_mkRecOn___spec__1(x_251, x_3, x_4, x_5, x_6, x_249);
+x_252 = l_Lean_ofExceptKernelException___at_Lean_mkCasesOn___spec__1(x_251, x_3, x_4, x_5, x_6, x_249);
 if (lean_obj_tag(x_252) == 0)
 {
 lean_object* x_253; lean_object* x_254; lean_object* x_255; 
@@ -4739,7 +3868,7 @@ x_256 = lean_ctor_get(x_255, 1);
 lean_inc(x_256);
 lean_dec(x_255);
 lean_inc(x_246);
-x_257 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4(x_246, x_20, x_3, x_4, x_5, x_6, x_256);
+x_257 = l_Lean_setReducibilityStatus___at_mkRecOn___spec__3(x_246, x_20, x_3, x_4, x_5, x_6, x_256);
 lean_dec(x_5);
 x_258 = lean_ctor_get(x_257, 1);
 lean_inc(x_258);
@@ -5011,7 +4140,7 @@ lean_inc(x_323);
 lean_inc(x_322);
 lean_inc(x_321);
 lean_dec(x_43);
-x_327 = l_Lean_mkRecOn___closed__2;
+x_327 = l_Lean_mkCasesOn___closed__7;
 x_328 = l_Lean_TagDeclarationExtension_tag(x_327, x_321, x_9);
 x_329 = lean_alloc_ctor(0, 7, 0);
 lean_ctor_set(x_329, 0, x_328);
@@ -5079,7 +4208,7 @@ lean_dec(x_346);
 x_349 = lean_mk_no_confusion(x_348, x_1);
 lean_dec(x_1);
 lean_inc(x_5);
-x_350 = l_Lean_ofExceptKernelException___at_Lean_mkRecOn___spec__1(x_349, x_3, x_4, x_5, x_6, x_347);
+x_350 = l_Lean_ofExceptKernelException___at_Lean_mkCasesOn___spec__1(x_349, x_3, x_4, x_5, x_6, x_347);
 if (lean_obj_tag(x_350) == 0)
 {
 lean_object* x_351; lean_object* x_352; lean_object* x_353; 
@@ -5098,7 +4227,7 @@ x_354 = lean_ctor_get(x_353, 1);
 lean_inc(x_354);
 lean_dec(x_353);
 lean_inc(x_344);
-x_355 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4(x_344, x_20, x_3, x_4, x_5, x_6, x_354);
+x_355 = l_Lean_setReducibilityStatus___at_mkRecOn___spec__3(x_344, x_20, x_3, x_4, x_5, x_6, x_354);
 lean_dec(x_5);
 x_356 = lean_ctor_get(x_355, 1);
 lean_inc(x_356);
@@ -5366,7 +4495,7 @@ lean_inc(x_421);
 lean_inc(x_420);
 lean_inc(x_419);
 lean_dec(x_35);
-x_423 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__5;
+x_423 = l_Lean_mkCasesOn___closed__6;
 x_424 = lean_alloc_ctor(0, 5, 0);
 lean_ctor_set(x_424, 0, x_419);
 lean_ctor_set(x_424, 1, x_423);
@@ -5408,7 +4537,7 @@ if (lean_is_exclusive(x_428)) {
  lean_dec_ref(x_428);
  x_436 = lean_box(0);
 }
-x_437 = l_Lean_mkRecOn___closed__2;
+x_437 = l_Lean_mkCasesOn___closed__7;
 x_438 = l_Lean_TagDeclarationExtension_tag(x_437, x_430, x_9);
 if (lean_is_scalar(x_436)) {
  x_439 = lean_alloc_ctor(0, 7, 0);
@@ -5480,7 +4609,7 @@ lean_dec(x_456);
 x_459 = lean_mk_no_confusion(x_458, x_1);
 lean_dec(x_1);
 lean_inc(x_5);
-x_460 = l_Lean_ofExceptKernelException___at_Lean_mkRecOn___spec__1(x_459, x_3, x_4, x_5, x_6, x_457);
+x_460 = l_Lean_ofExceptKernelException___at_Lean_mkCasesOn___spec__1(x_459, x_3, x_4, x_5, x_6, x_457);
 if (lean_obj_tag(x_460) == 0)
 {
 lean_object* x_461; lean_object* x_462; lean_object* x_463; 
@@ -5499,7 +4628,7 @@ x_464 = lean_ctor_get(x_463, 1);
 lean_inc(x_464);
 lean_dec(x_463);
 lean_inc(x_454);
-x_465 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4(x_454, x_20, x_3, x_4, x_5, x_6, x_464);
+x_465 = l_Lean_setReducibilityStatus___at_mkRecOn___spec__3(x_454, x_20, x_3, x_4, x_5, x_6, x_464);
 lean_dec(x_5);
 x_466 = lean_ctor_get(x_465, 1);
 lean_inc(x_466);
@@ -5774,7 +4903,7 @@ lean_dec(x_24);
 x_535 = l___private_Lean_Meta_Constructions_0__Lean_mkBelowOrIBelow___lambda__1___closed__1;
 lean_inc(x_9);
 x_536 = l_Lean_TagDeclarationExtension_tag(x_535, x_529, x_9);
-x_537 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__3;
+x_537 = l_Lean_mkCasesOn___closed__4;
 x_538 = lean_alloc_ctor(0, 7, 0);
 lean_ctor_set(x_538, 0, x_536);
 lean_ctor_set(x_538, 1, x_530);
@@ -5812,7 +4941,7 @@ if (lean_is_exclusive(x_542)) {
  lean_dec_ref(x_542);
  x_548 = lean_box(0);
 }
-x_549 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__5;
+x_549 = l_Lean_mkCasesOn___closed__6;
 if (lean_is_scalar(x_548)) {
  x_550 = lean_alloc_ctor(0, 5, 0);
 } else {
@@ -5858,7 +4987,7 @@ if (lean_is_exclusive(x_554)) {
  lean_dec_ref(x_554);
  x_562 = lean_box(0);
 }
-x_563 = l_Lean_mkRecOn___closed__2;
+x_563 = l_Lean_mkCasesOn___closed__7;
 x_564 = l_Lean_TagDeclarationExtension_tag(x_563, x_556, x_9);
 if (lean_is_scalar(x_562)) {
  x_565 = lean_alloc_ctor(0, 7, 0);
@@ -5930,7 +5059,7 @@ lean_dec(x_582);
 x_585 = lean_mk_no_confusion(x_584, x_1);
 lean_dec(x_1);
 lean_inc(x_5);
-x_586 = l_Lean_ofExceptKernelException___at_Lean_mkRecOn___spec__1(x_585, x_3, x_4, x_5, x_6, x_583);
+x_586 = l_Lean_ofExceptKernelException___at_Lean_mkCasesOn___spec__1(x_585, x_3, x_4, x_5, x_6, x_583);
 if (lean_obj_tag(x_586) == 0)
 {
 lean_object* x_587; lean_object* x_588; lean_object* x_589; 
@@ -5949,7 +5078,7 @@ x_590 = lean_ctor_get(x_589, 1);
 lean_inc(x_590);
 lean_dec(x_589);
 lean_inc(x_580);
-x_591 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4(x_580, x_20, x_3, x_4, x_5, x_6, x_590);
+x_591 = l_Lean_setReducibilityStatus___at_mkRecOn___spec__3(x_580, x_20, x_3, x_4, x_5, x_6, x_590);
 lean_dec(x_5);
 x_592 = lean_ctor_get(x_591, 1);
 lean_inc(x_592);
@@ -6621,7 +5750,7 @@ x_40 = lean_ctor_get(x_39, 1);
 lean_inc(x_40);
 lean_dec(x_39);
 x_41 = 0;
-x_42 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4(x_5, x_41, x_10, x_11, x_12, x_13, x_40);
+x_42 = l_Lean_setReducibilityStatus___at_mkRecOn___spec__3(x_5, x_41, x_10, x_11, x_12, x_13, x_40);
 lean_dec(x_13);
 lean_dec(x_12);
 return x_42;
@@ -6745,7 +5874,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; 
 x_1 = l_Lean_mkNoConfusionEnum_mkToCtorIdx___closed__1;
 x_2 = l_Lean_mkNoConfusionEnum_mkToCtorIdx___closed__2;
-x_3 = lean_unsigned_to_nat(116u);
+x_3 = lean_unsigned_to_nat(108u);
 x_4 = lean_unsigned_to_nat(63u);
 x_5 = l_Lean_mkNoConfusionEnum_mkToCtorIdx___closed__3;
 x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@@ -7078,7 +6207,7 @@ x_47 = lean_ctor_get(x_46, 1);
 lean_inc(x_47);
 lean_dec(x_46);
 x_48 = 0;
-x_49 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4(x_37, x_48, x_9, x_10, x_11, x_12, x_47);
+x_49 = l_Lean_setReducibilityStatus___at_mkRecOn___spec__3(x_37, x_48, x_9, x_10, x_11, x_12, x_47);
 lean_dec(x_12);
 lean_dec(x_11);
 lean_dec(x_10);
@@ -7283,7 +6412,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; 
 x_1 = l_Lean_mkNoConfusionEnum_mkToCtorIdx___closed__1;
 x_2 = l_Lean_mkNoConfusionEnum_mkNoConfusionType___closed__1;
-x_3 = lean_unsigned_to_nat(140u);
+x_3 = lean_unsigned_to_nat(132u);
 x_4 = lean_unsigned_to_nat(63u);
 x_5 = l_Lean_mkNoConfusionEnum_mkToCtorIdx___closed__3;
 x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@@ -7589,7 +6718,7 @@ lean_inc(x_56);
 lean_dec(x_55);
 x_57 = 0;
 lean_inc(x_46);
-x_58 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4(x_46, x_57, x_10, x_11, x_12, x_13, x_56);
+x_58 = l_Lean_setReducibilityStatus___at_mkRecOn___spec__3(x_46, x_57, x_10, x_11, x_12, x_13, x_56);
 lean_dec(x_12);
 lean_dec(x_10);
 x_59 = lean_ctor_get(x_58, 1);
@@ -7610,7 +6739,7 @@ x_65 = lean_ctor_get(x_61, 4);
 lean_dec(x_65);
 x_66 = l_Lean_mkNoConfusionCore___lambda__1___closed__3;
 x_67 = l_Lean_TagDeclarationExtension_tag(x_66, x_64, x_46);
-x_68 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__3;
+x_68 = l_Lean_mkCasesOn___closed__4;
 lean_ctor_set(x_61, 4, x_68);
 lean_ctor_set(x_61, 0, x_67);
 x_69 = lean_st_ref_set(x_13, x_61, x_62);
@@ -7630,7 +6759,7 @@ if (x_74 == 0)
 lean_object* x_75; lean_object* x_76; lean_object* x_77; uint8_t x_78; 
 x_75 = lean_ctor_get(x_72, 1);
 lean_dec(x_75);
-x_76 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__5;
+x_76 = l_Lean_mkCasesOn___closed__6;
 lean_ctor_set(x_72, 1, x_76);
 x_77 = lean_st_ref_set(x_11, x_72, x_73);
 lean_dec(x_11);
@@ -7669,7 +6798,7 @@ lean_inc(x_86);
 lean_inc(x_85);
 lean_inc(x_84);
 lean_dec(x_72);
-x_88 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__5;
+x_88 = l_Lean_mkCasesOn___closed__6;
 x_89 = lean_alloc_ctor(0, 5, 0);
 lean_ctor_set(x_89, 0, x_84);
 lean_ctor_set(x_89, 1, x_88);
@@ -7717,7 +6846,7 @@ lean_inc(x_95);
 lean_dec(x_61);
 x_101 = l_Lean_mkNoConfusionCore___lambda__1___closed__3;
 x_102 = l_Lean_TagDeclarationExtension_tag(x_101, x_95, x_46);
-x_103 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__3;
+x_103 = l_Lean_mkCasesOn___closed__4;
 x_104 = lean_alloc_ctor(0, 7, 0);
 lean_ctor_set(x_104, 0, x_102);
 lean_ctor_set(x_104, 1, x_96);
@@ -7756,7 +6885,7 @@ if (lean_is_exclusive(x_108)) {
  lean_dec_ref(x_108);
  x_114 = lean_box(0);
 }
-x_115 = l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__5;
+x_115 = l_Lean_mkCasesOn___closed__6;
 if (lean_is_scalar(x_114)) {
  x_116 = lean_alloc_ctor(0, 5, 0);
 } else {
@@ -8059,7 +7188,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; 
 x_1 = l_Lean_mkNoConfusionEnum_mkToCtorIdx___closed__1;
 x_2 = l_Lean_mkNoConfusionEnum_mkNoConfusion___closed__1;
-x_3 = lean_unsigned_to_nat(163u);
+x_3 = lean_unsigned_to_nat(155u);
 x_4 = lean_unsigned_to_nat(63u);
 x_5 = l_Lean_mkNoConfusionEnum_mkToCtorIdx___closed__3;
 x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@@ -8922,6 +8051,7 @@ lean_object* initialize_Lean_AuxRecursor(uint8_t builtin, lean_object*);
 lean_object* initialize_Lean_AddDecl(uint8_t builtin, lean_object*);
 lean_object* initialize_Lean_Meta_AppBuilder(uint8_t builtin, lean_object*);
 lean_object* initialize_Lean_Meta_CompletionName(uint8_t builtin, lean_object*);
+lean_object* initialize_Lean_Meta_Constructions_RecOn(uint8_t builtin, lean_object*);
 static bool _G_initialized = false;
 LEAN_EXPORT lean_object* initialize_Lean_Meta_Constructions(uint8_t builtin, lean_object* w) {
 lean_object * res;
@@ -8939,20 +8069,23 @@ lean_dec_ref(res);
 res = initialize_Lean_Meta_CompletionName(builtin, lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
-l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__1 = _init_l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__1();
-lean_mark_persistent(l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__1);
-l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__2 = _init_l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__2();
-lean_mark_persistent(l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__2);
-l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__3 = _init_l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__3();
-lean_mark_persistent(l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__3);
-l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__4 = _init_l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__4();
-lean_mark_persistent(l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__4);
-l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__5 = _init_l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__5();
-lean_mark_persistent(l_Lean_setReducibilityStatus___at_Lean_mkRecOn___spec__4___closed__5);
-l_Lean_mkRecOn___closed__1 = _init_l_Lean_mkRecOn___closed__1();
-lean_mark_persistent(l_Lean_mkRecOn___closed__1);
-l_Lean_mkRecOn___closed__2 = _init_l_Lean_mkRecOn___closed__2();
-lean_mark_persistent(l_Lean_mkRecOn___closed__2);
+res = initialize_Lean_Meta_Constructions_RecOn(builtin, lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+l_Lean_mkCasesOn___closed__1 = _init_l_Lean_mkCasesOn___closed__1();
+lean_mark_persistent(l_Lean_mkCasesOn___closed__1);
+l_Lean_mkCasesOn___closed__2 = _init_l_Lean_mkCasesOn___closed__2();
+lean_mark_persistent(l_Lean_mkCasesOn___closed__2);
+l_Lean_mkCasesOn___closed__3 = _init_l_Lean_mkCasesOn___closed__3();
+lean_mark_persistent(l_Lean_mkCasesOn___closed__3);
+l_Lean_mkCasesOn___closed__4 = _init_l_Lean_mkCasesOn___closed__4();
+lean_mark_persistent(l_Lean_mkCasesOn___closed__4);
+l_Lean_mkCasesOn___closed__5 = _init_l_Lean_mkCasesOn___closed__5();
+lean_mark_persistent(l_Lean_mkCasesOn___closed__5);
+l_Lean_mkCasesOn___closed__6 = _init_l_Lean_mkCasesOn___closed__6();
+lean_mark_persistent(l_Lean_mkCasesOn___closed__6);
+l_Lean_mkCasesOn___closed__7 = _init_l_Lean_mkCasesOn___closed__7();
+lean_mark_persistent(l_Lean_mkCasesOn___closed__7);
 l___private_Lean_Meta_Constructions_0__Lean_mkBelowOrIBelow___lambda__1___closed__1 = _init_l___private_Lean_Meta_Constructions_0__Lean_mkBelowOrIBelow___lambda__1___closed__1();
 lean_mark_persistent(l___private_Lean_Meta_Constructions_0__Lean_mkBelowOrIBelow___lambda__1___closed__1);
 l___private_Lean_Meta_Constructions_0__Lean_mkBRecOrBInductionOn___lambda__2___closed__1 = _init_l___private_Lean_Meta_Constructions_0__Lean_mkBRecOrBInductionOn___lambda__2___closed__1();
diff --git a/stage0/stdlib/Lean/Meta/Constructions/RecOn.c b/stage0/stdlib/Lean/Meta/Constructions/RecOn.c
new file mode 100644
index 0000000000..b4bb4a27fa
--- /dev/null
+++ b/stage0/stdlib/Lean/Meta/Constructions/RecOn.c
@@ -0,0 +1,1832 @@
+// Lean compiler output
+// Module: Lean.Meta.Constructions.RecOn
+// Imports: Lean.Meta.InferType Lean.AuxRecursor Lean.AddDecl Lean.Meta.CompletionName
+#include <lean/lean.h>
+#if defined(__clang__)
+#pragma clang diagnostic ignored "-Wunused-parameter"
+#pragma clang diagnostic ignored "-Wunused-label"
+#elif defined(__GNUC__) && !defined(__CLANG__)
+#pragma GCC diagnostic ignored "-Wunused-parameter"
+#pragma GCC diagnostic ignored "-Wunused-label"
+#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
+#endif
+#ifdef __cplusplus
+extern "C" {
+#endif
+lean_object* l_Lean_Expr_const___override(lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_List_map___at_mkRecOn___spec__1(lean_object*);
+lean_object* l_Lean_getConstInfo___at_Lean_Meta_mkConstWithFreshMVarLevels___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_mkAppN(lean_object*, lean_object*);
+lean_object* l_Array_toSubarray___rarg(lean_object*, lean_object*, lean_object*);
+static lean_object* l_Lean_setReducibilityStatus___at_mkRecOn___spec__3___closed__4;
+lean_object* l_Lean_Meta_forallTelescope___at_Lean_Meta_mapForallTelescope_x27___spec__1___rarg(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+static lean_object* l_mkRecOn___closed__2;
+extern lean_object* l_Lean_auxRecExt;
+static lean_object* l_Lean_setReducibilityStatus___at_mkRecOn___spec__3___closed__2;
+lean_object* l_Lean_stringToMessageData(lean_object*);
+lean_object* l_Lean_throwError___at_Lean_Meta_setInlineAttribute___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+static lean_object* l_mkRecOn___closed__3;
+static lean_object* l_mkRecOn___closed__7;
+lean_object* lean_st_ref_take(lean_object*, lean_object*);
+static lean_object* l_mkRecOn___closed__1;
+LEAN_EXPORT lean_object* l_mkRecOn___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* lean_st_ref_get(lean_object*, lean_object*);
+static lean_object* l_mkRecOn___closed__4;
+LEAN_EXPORT lean_object* l_Lean_mkDefinitionValInferrringUnsafe___at_mkRecOn___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Name_str___override(lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_mkRecOn___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+static lean_object* l_Lean_setReducibilityStatus___at_mkRecOn___spec__3___closed__3;
+lean_object* l___private_Lean_ReducibilityAttrs_0__Lean_setReducibilityStatusCore(lean_object*, lean_object*, uint8_t, uint8_t, lean_object*);
+static lean_object* l_Lean_setReducibilityStatus___at_mkRecOn___spec__3___closed__5;
+uint8_t l_Lean_Environment_hasUnsafe(lean_object*, lean_object*);
+extern lean_object* l_Lean_recOnSuffix;
+lean_object* l_Array_append___rarg(lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Lean_setReducibilityStatus___at_mkRecOn___spec__3(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Lean_mkDefinitionValInferrringUnsafe___at_mkRecOn___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_TagDeclarationExtension_tag(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Meta_mkForallFVars(lean_object*, lean_object*, uint8_t, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+static lean_object* l_Lean_setReducibilityStatus___at_mkRecOn___spec__3___closed__1;
+lean_object* lean_nat_sub(lean_object*, lean_object*);
+static lean_object* l_mkRecOn___closed__6;
+lean_object* l_Lean_PersistentHashMap_mkEmptyEntriesArray(lean_object*, lean_object*);
+lean_object* l_Array_ofSubarray___rarg(lean_object*);
+extern lean_object* l_Lean_protectedExt;
+lean_object* l_Lean_Level_param___override(lean_object*);
+lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
+lean_object* lean_array_get_size(lean_object*);
+lean_object* l_Lean_Meta_mkLambdaFVars(lean_object*, lean_object*, uint8_t, uint8_t, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* lean_nat_add(lean_object*, lean_object*);
+lean_object* l_Lean_MessageData_ofName(lean_object*);
+static lean_object* l_mkRecOn___closed__5;
+LEAN_EXPORT lean_object* l_Lean_setReducibilityStatus___at_mkRecOn___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_mkRecOn(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_addDecl(lean_object*, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_List_map___at_mkRecOn___spec__1(lean_object* x_1) {
+_start:
+{
+if (lean_obj_tag(x_1) == 0)
+{
+lean_object* x_2; 
+x_2 = lean_box(0);
+return x_2;
+}
+else
+{
+uint8_t x_3; 
+x_3 = !lean_is_exclusive(x_1);
+if (x_3 == 0)
+{
+lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
+x_4 = lean_ctor_get(x_1, 0);
+x_5 = lean_ctor_get(x_1, 1);
+x_6 = l_Lean_Level_param___override(x_4);
+x_7 = l_List_map___at_mkRecOn___spec__1(x_5);
+lean_ctor_set(x_1, 1, x_7);
+lean_ctor_set(x_1, 0, x_6);
+return x_1;
+}
+else
+{
+lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; 
+x_8 = lean_ctor_get(x_1, 0);
+x_9 = lean_ctor_get(x_1, 1);
+lean_inc(x_9);
+lean_inc(x_8);
+lean_dec(x_1);
+x_10 = l_Lean_Level_param___override(x_8);
+x_11 = l_List_map___at_mkRecOn___spec__1(x_9);
+x_12 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_12, 0, x_10);
+lean_ctor_set(x_12, 1, x_11);
+return x_12;
+}
+}
+}
+}
+LEAN_EXPORT lean_object* l_Lean_mkDefinitionValInferrringUnsafe___at_mkRecOn___spec__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
+_start:
+{
+lean_object* x_11; uint8_t x_12; 
+x_11 = lean_st_ref_get(x_9, x_10);
+x_12 = !lean_is_exclusive(x_11);
+if (x_12 == 0)
+{
+lean_object* x_13; lean_object* x_14; uint8_t x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; 
+x_13 = lean_ctor_get(x_11, 0);
+x_14 = lean_ctor_get(x_13, 0);
+lean_inc(x_14);
+lean_dec(x_13);
+lean_inc(x_3);
+lean_inc(x_14);
+x_15 = l_Lean_Environment_hasUnsafe(x_14, x_3);
+lean_inc(x_1);
+x_16 = lean_alloc_ctor(0, 3, 0);
+lean_ctor_set(x_16, 0, x_1);
+lean_ctor_set(x_16, 1, x_2);
+lean_ctor_set(x_16, 2, x_3);
+x_17 = lean_box(0);
+x_18 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_18, 0, x_1);
+lean_ctor_set(x_18, 1, x_17);
+if (x_15 == 0)
+{
+uint8_t x_19; 
+lean_inc(x_4);
+x_19 = l_Lean_Environment_hasUnsafe(x_14, x_4);
+if (x_19 == 0)
+{
+uint8_t x_20; lean_object* x_21; 
+x_20 = 1;
+x_21 = lean_alloc_ctor(0, 4, 1);
+lean_ctor_set(x_21, 0, x_16);
+lean_ctor_set(x_21, 1, x_4);
+lean_ctor_set(x_21, 2, x_5);
+lean_ctor_set(x_21, 3, x_18);
+lean_ctor_set_uint8(x_21, sizeof(void*)*4, x_20);
+lean_ctor_set(x_11, 0, x_21);
+return x_11;
+}
+else
+{
+uint8_t x_22; lean_object* x_23; 
+x_22 = 0;
+x_23 = lean_alloc_ctor(0, 4, 1);
+lean_ctor_set(x_23, 0, x_16);
+lean_ctor_set(x_23, 1, x_4);
+lean_ctor_set(x_23, 2, x_5);
+lean_ctor_set(x_23, 3, x_18);
+lean_ctor_set_uint8(x_23, sizeof(void*)*4, x_22);
+lean_ctor_set(x_11, 0, x_23);
+return x_11;
+}
+}
+else
+{
+uint8_t x_24; lean_object* x_25; 
+lean_dec(x_14);
+x_24 = 0;
+x_25 = lean_alloc_ctor(0, 4, 1);
+lean_ctor_set(x_25, 0, x_16);
+lean_ctor_set(x_25, 1, x_4);
+lean_ctor_set(x_25, 2, x_5);
+lean_ctor_set(x_25, 3, x_18);
+lean_ctor_set_uint8(x_25, sizeof(void*)*4, x_24);
+lean_ctor_set(x_11, 0, x_25);
+return x_11;
+}
+}
+else
+{
+lean_object* x_26; lean_object* x_27; lean_object* x_28; uint8_t x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; 
+x_26 = lean_ctor_get(x_11, 0);
+x_27 = lean_ctor_get(x_11, 1);
+lean_inc(x_27);
+lean_inc(x_26);
+lean_dec(x_11);
+x_28 = lean_ctor_get(x_26, 0);
+lean_inc(x_28);
+lean_dec(x_26);
+lean_inc(x_3);
+lean_inc(x_28);
+x_29 = l_Lean_Environment_hasUnsafe(x_28, x_3);
+lean_inc(x_1);
+x_30 = lean_alloc_ctor(0, 3, 0);
+lean_ctor_set(x_30, 0, x_1);
+lean_ctor_set(x_30, 1, x_2);
+lean_ctor_set(x_30, 2, x_3);
+x_31 = lean_box(0);
+x_32 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_32, 0, x_1);
+lean_ctor_set(x_32, 1, x_31);
+if (x_29 == 0)
+{
+uint8_t x_33; 
+lean_inc(x_4);
+x_33 = l_Lean_Environment_hasUnsafe(x_28, x_4);
+if (x_33 == 0)
+{
+uint8_t x_34; lean_object* x_35; lean_object* x_36; 
+x_34 = 1;
+x_35 = lean_alloc_ctor(0, 4, 1);
+lean_ctor_set(x_35, 0, x_30);
+lean_ctor_set(x_35, 1, x_4);
+lean_ctor_set(x_35, 2, x_5);
+lean_ctor_set(x_35, 3, x_32);
+lean_ctor_set_uint8(x_35, sizeof(void*)*4, x_34);
+x_36 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_36, 0, x_35);
+lean_ctor_set(x_36, 1, x_27);
+return x_36;
+}
+else
+{
+uint8_t x_37; lean_object* x_38; lean_object* x_39; 
+x_37 = 0;
+x_38 = lean_alloc_ctor(0, 4, 1);
+lean_ctor_set(x_38, 0, x_30);
+lean_ctor_set(x_38, 1, x_4);
+lean_ctor_set(x_38, 2, x_5);
+lean_ctor_set(x_38, 3, x_32);
+lean_ctor_set_uint8(x_38, sizeof(void*)*4, x_37);
+x_39 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_39, 0, x_38);
+lean_ctor_set(x_39, 1, x_27);
+return x_39;
+}
+}
+else
+{
+uint8_t x_40; lean_object* x_41; lean_object* x_42; 
+lean_dec(x_28);
+x_40 = 0;
+x_41 = lean_alloc_ctor(0, 4, 1);
+lean_ctor_set(x_41, 0, x_30);
+lean_ctor_set(x_41, 1, x_4);
+lean_ctor_set(x_41, 2, x_5);
+lean_ctor_set(x_41, 3, x_32);
+lean_ctor_set_uint8(x_41, sizeof(void*)*4, x_40);
+x_42 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_42, 0, x_41);
+lean_ctor_set(x_42, 1, x_27);
+return x_42;
+}
+}
+}
+}
+static lean_object* _init_l_Lean_setReducibilityStatus___at_mkRecOn___spec__3___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = l_Lean_PersistentHashMap_mkEmptyEntriesArray(lean_box(0), lean_box(0));
+return x_1;
+}
+}
+static lean_object* _init_l_Lean_setReducibilityStatus___at_mkRecOn___spec__3___closed__2() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_Lean_setReducibilityStatus___at_mkRecOn___spec__3___closed__1;
+x_2 = lean_alloc_ctor(0, 1, 0);
+lean_ctor_set(x_2, 0, x_1);
+return x_2;
+}
+}
+static lean_object* _init_l_Lean_setReducibilityStatus___at_mkRecOn___spec__3___closed__3() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_Lean_setReducibilityStatus___at_mkRecOn___spec__3___closed__2;
+x_2 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_2, 0, x_1);
+lean_ctor_set(x_2, 1, x_1);
+return x_2;
+}
+}
+static lean_object* _init_l_Lean_setReducibilityStatus___at_mkRecOn___spec__3___closed__4() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_Lean_setReducibilityStatus___at_mkRecOn___spec__3___closed__2;
+x_2 = lean_alloc_ctor(0, 4, 0);
+lean_ctor_set(x_2, 0, x_1);
+lean_ctor_set(x_2, 1, x_1);
+lean_ctor_set(x_2, 2, x_1);
+lean_ctor_set(x_2, 3, x_1);
+return x_2;
+}
+}
+static lean_object* _init_l_Lean_setReducibilityStatus___at_mkRecOn___spec__3___closed__5() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_setReducibilityStatus___at_mkRecOn___spec__3___closed__2;
+x_2 = l_Lean_setReducibilityStatus___at_mkRecOn___spec__3___closed__4;
+x_3 = lean_alloc_ctor(0, 7, 0);
+lean_ctor_set(x_3, 0, x_1);
+lean_ctor_set(x_3, 1, x_1);
+lean_ctor_set(x_3, 2, x_1);
+lean_ctor_set(x_3, 3, x_1);
+lean_ctor_set(x_3, 4, x_1);
+lean_ctor_set(x_3, 5, x_2);
+lean_ctor_set(x_3, 6, x_2);
+return x_3;
+}
+}
+LEAN_EXPORT lean_object* l_Lean_setReducibilityStatus___at_mkRecOn___spec__3(lean_object* x_1, uint8_t x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
+_start:
+{
+lean_object* x_8; lean_object* x_9; lean_object* x_10; uint8_t x_11; 
+x_8 = lean_st_ref_take(x_6, x_7);
+x_9 = lean_ctor_get(x_8, 0);
+lean_inc(x_9);
+x_10 = lean_ctor_get(x_8, 1);
+lean_inc(x_10);
+lean_dec(x_8);
+x_11 = !lean_is_exclusive(x_9);
+if (x_11 == 0)
+{
+lean_object* x_12; lean_object* x_13; uint8_t x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; uint8_t x_23; 
+x_12 = lean_ctor_get(x_9, 0);
+x_13 = lean_ctor_get(x_9, 4);
+lean_dec(x_13);
+x_14 = 0;
+x_15 = lean_box(0);
+x_16 = l___private_Lean_ReducibilityAttrs_0__Lean_setReducibilityStatusCore(x_12, x_1, x_2, x_14, x_15);
+x_17 = l_Lean_setReducibilityStatus___at_mkRecOn___spec__3___closed__3;
+lean_ctor_set(x_9, 4, x_17);
+lean_ctor_set(x_9, 0, x_16);
+x_18 = lean_st_ref_set(x_6, x_9, x_10);
+x_19 = lean_ctor_get(x_18, 1);
+lean_inc(x_19);
+lean_dec(x_18);
+x_20 = lean_st_ref_take(x_4, x_19);
+x_21 = lean_ctor_get(x_20, 0);
+lean_inc(x_21);
+x_22 = lean_ctor_get(x_20, 1);
+lean_inc(x_22);
+lean_dec(x_20);
+x_23 = !lean_is_exclusive(x_21);
+if (x_23 == 0)
+{
+lean_object* x_24; lean_object* x_25; lean_object* x_26; uint8_t x_27; 
+x_24 = lean_ctor_get(x_21, 1);
+lean_dec(x_24);
+x_25 = l_Lean_setReducibilityStatus___at_mkRecOn___spec__3___closed__5;
+lean_ctor_set(x_21, 1, x_25);
+x_26 = lean_st_ref_set(x_4, x_21, x_22);
+x_27 = !lean_is_exclusive(x_26);
+if (x_27 == 0)
+{
+lean_object* x_28; lean_object* x_29; 
+x_28 = lean_ctor_get(x_26, 0);
+lean_dec(x_28);
+x_29 = lean_box(0);
+lean_ctor_set(x_26, 0, x_29);
+return x_26;
+}
+else
+{
+lean_object* x_30; lean_object* x_31; lean_object* x_32; 
+x_30 = lean_ctor_get(x_26, 1);
+lean_inc(x_30);
+lean_dec(x_26);
+x_31 = lean_box(0);
+x_32 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_32, 0, x_31);
+lean_ctor_set(x_32, 1, x_30);
+return x_32;
+}
+}
+else
+{
+lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; 
+x_33 = lean_ctor_get(x_21, 0);
+x_34 = lean_ctor_get(x_21, 2);
+x_35 = lean_ctor_get(x_21, 3);
+x_36 = lean_ctor_get(x_21, 4);
+lean_inc(x_36);
+lean_inc(x_35);
+lean_inc(x_34);
+lean_inc(x_33);
+lean_dec(x_21);
+x_37 = l_Lean_setReducibilityStatus___at_mkRecOn___spec__3___closed__5;
+x_38 = lean_alloc_ctor(0, 5, 0);
+lean_ctor_set(x_38, 0, x_33);
+lean_ctor_set(x_38, 1, x_37);
+lean_ctor_set(x_38, 2, x_34);
+lean_ctor_set(x_38, 3, x_35);
+lean_ctor_set(x_38, 4, x_36);
+x_39 = lean_st_ref_set(x_4, x_38, x_22);
+x_40 = lean_ctor_get(x_39, 1);
+lean_inc(x_40);
+if (lean_is_exclusive(x_39)) {
+ lean_ctor_release(x_39, 0);
+ lean_ctor_release(x_39, 1);
+ x_41 = x_39;
+} else {
+ lean_dec_ref(x_39);
+ x_41 = lean_box(0);
+}
+x_42 = lean_box(0);
+if (lean_is_scalar(x_41)) {
+ x_43 = lean_alloc_ctor(0, 2, 0);
+} else {
+ x_43 = x_41;
+}
+lean_ctor_set(x_43, 0, x_42);
+lean_ctor_set(x_43, 1, x_40);
+return x_43;
+}
+}
+else
+{
+lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; uint8_t x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_71; 
+x_44 = lean_ctor_get(x_9, 0);
+x_45 = lean_ctor_get(x_9, 1);
+x_46 = lean_ctor_get(x_9, 2);
+x_47 = lean_ctor_get(x_9, 3);
+x_48 = lean_ctor_get(x_9, 5);
+x_49 = lean_ctor_get(x_9, 6);
+lean_inc(x_49);
+lean_inc(x_48);
+lean_inc(x_47);
+lean_inc(x_46);
+lean_inc(x_45);
+lean_inc(x_44);
+lean_dec(x_9);
+x_50 = 0;
+x_51 = lean_box(0);
+x_52 = l___private_Lean_ReducibilityAttrs_0__Lean_setReducibilityStatusCore(x_44, x_1, x_2, x_50, x_51);
+x_53 = l_Lean_setReducibilityStatus___at_mkRecOn___spec__3___closed__3;
+x_54 = lean_alloc_ctor(0, 7, 0);
+lean_ctor_set(x_54, 0, x_52);
+lean_ctor_set(x_54, 1, x_45);
+lean_ctor_set(x_54, 2, x_46);
+lean_ctor_set(x_54, 3, x_47);
+lean_ctor_set(x_54, 4, x_53);
+lean_ctor_set(x_54, 5, x_48);
+lean_ctor_set(x_54, 6, x_49);
+x_55 = lean_st_ref_set(x_6, x_54, x_10);
+x_56 = lean_ctor_get(x_55, 1);
+lean_inc(x_56);
+lean_dec(x_55);
+x_57 = lean_st_ref_take(x_4, x_56);
+x_58 = lean_ctor_get(x_57, 0);
+lean_inc(x_58);
+x_59 = lean_ctor_get(x_57, 1);
+lean_inc(x_59);
+lean_dec(x_57);
+x_60 = lean_ctor_get(x_58, 0);
+lean_inc(x_60);
+x_61 = lean_ctor_get(x_58, 2);
+lean_inc(x_61);
+x_62 = lean_ctor_get(x_58, 3);
+lean_inc(x_62);
+x_63 = lean_ctor_get(x_58, 4);
+lean_inc(x_63);
+if (lean_is_exclusive(x_58)) {
+ lean_ctor_release(x_58, 0);
+ lean_ctor_release(x_58, 1);
+ lean_ctor_release(x_58, 2);
+ lean_ctor_release(x_58, 3);
+ lean_ctor_release(x_58, 4);
+ x_64 = x_58;
+} else {
+ lean_dec_ref(x_58);
+ x_64 = lean_box(0);
+}
+x_65 = l_Lean_setReducibilityStatus___at_mkRecOn___spec__3___closed__5;
+if (lean_is_scalar(x_64)) {
+ x_66 = lean_alloc_ctor(0, 5, 0);
+} else {
+ x_66 = x_64;
+}
+lean_ctor_set(x_66, 0, x_60);
+lean_ctor_set(x_66, 1, x_65);
+lean_ctor_set(x_66, 2, x_61);
+lean_ctor_set(x_66, 3, x_62);
+lean_ctor_set(x_66, 4, x_63);
+x_67 = lean_st_ref_set(x_4, x_66, x_59);
+x_68 = lean_ctor_get(x_67, 1);
+lean_inc(x_68);
+if (lean_is_exclusive(x_67)) {
+ lean_ctor_release(x_67, 0);
+ lean_ctor_release(x_67, 1);
+ x_69 = x_67;
+} else {
+ lean_dec_ref(x_67);
+ x_69 = lean_box(0);
+}
+x_70 = lean_box(0);
+if (lean_is_scalar(x_69)) {
+ x_71 = lean_alloc_ctor(0, 2, 0);
+} else {
+ x_71 = x_69;
+}
+lean_ctor_set(x_71, 0, x_70);
+lean_ctor_set(x_71, 1, x_68);
+return x_71;
+}
+}
+}
+LEAN_EXPORT lean_object* l_mkRecOn___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
+_start:
+{
+lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; uint8_t x_41; uint8_t x_42; uint8_t x_43; lean_object* x_44; 
+x_11 = lean_ctor_get(x_1, 0);
+lean_inc(x_11);
+x_12 = lean_ctor_get(x_1, 1);
+lean_inc(x_12);
+lean_dec(x_1);
+lean_inc(x_12);
+x_13 = l_List_map___at_mkRecOn___spec__1(x_12);
+x_14 = l_Lean_Expr_const___override(x_11, x_13);
+x_15 = l_Lean_mkAppN(x_14, x_4);
+x_16 = lean_array_get_size(x_4);
+x_17 = lean_ctor_get(x_2, 5);
+x_18 = lean_nat_sub(x_16, x_17);
+lean_dec(x_16);
+x_19 = lean_ctor_get(x_2, 3);
+x_20 = lean_nat_sub(x_18, x_19);
+lean_dec(x_18);
+x_21 = lean_unsigned_to_nat(1u);
+x_22 = lean_nat_sub(x_20, x_21);
+lean_dec(x_20);
+x_23 = lean_unsigned_to_nat(0u);
+lean_inc(x_22);
+lean_inc(x_4);
+x_24 = l_Array_toSubarray___rarg(x_4, x_23, x_22);
+x_25 = lean_nat_add(x_22, x_17);
+x_26 = lean_nat_add(x_25, x_21);
+x_27 = lean_nat_add(x_26, x_19);
+lean_dec(x_26);
+lean_inc(x_25);
+lean_inc(x_4);
+x_28 = l_Array_toSubarray___rarg(x_4, x_25, x_27);
+x_29 = l_Array_ofSubarray___rarg(x_24);
+lean_dec(x_24);
+x_30 = l_Array_ofSubarray___rarg(x_28);
+lean_dec(x_28);
+x_31 = l_Array_append___rarg(x_29, x_30);
+lean_dec(x_30);
+x_32 = lean_array_get_size(x_31);
+x_33 = l_Array_toSubarray___rarg(x_31, x_23, x_32);
+x_34 = l_Array_toSubarray___rarg(x_4, x_22, x_25);
+x_35 = l_Array_ofSubarray___rarg(x_33);
+lean_dec(x_33);
+x_36 = l_Array_ofSubarray___rarg(x_34);
+lean_dec(x_34);
+x_37 = l_Array_append___rarg(x_35, x_36);
+lean_dec(x_36);
+x_38 = lean_array_get_size(x_37);
+x_39 = l_Array_toSubarray___rarg(x_37, x_23, x_38);
+x_40 = l_Array_ofSubarray___rarg(x_39);
+lean_dec(x_39);
+x_41 = 0;
+x_42 = 1;
+x_43 = 1;
+lean_inc(x_40);
+x_44 = l_Lean_Meta_mkForallFVars(x_40, x_5, x_41, x_42, x_43, x_6, x_7, x_8, x_9, x_10);
+if (lean_obj_tag(x_44) == 0)
+{
+lean_object* x_45; lean_object* x_46; lean_object* x_47; 
+x_45 = lean_ctor_get(x_44, 0);
+lean_inc(x_45);
+x_46 = lean_ctor_get(x_44, 1);
+lean_inc(x_46);
+lean_dec(x_44);
+x_47 = l_Lean_Meta_mkLambdaFVars(x_40, x_15, x_41, x_42, x_41, x_43, x_6, x_7, x_8, x_9, x_46);
+if (lean_obj_tag(x_47) == 0)
+{
+lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; 
+x_48 = lean_ctor_get(x_47, 0);
+lean_inc(x_48);
+x_49 = lean_ctor_get(x_47, 1);
+lean_inc(x_49);
+lean_dec(x_47);
+x_50 = l_Lean_recOnSuffix;
+x_51 = l_Lean_Name_str___override(x_3, x_50);
+x_52 = lean_box(1);
+x_53 = l_Lean_mkDefinitionValInferrringUnsafe___at_mkRecOn___spec__2(x_51, x_12, x_45, x_48, x_52, x_6, x_7, x_8, x_9, x_49);
+return x_53;
+}
+else
+{
+uint8_t x_54; 
+lean_dec(x_45);
+lean_dec(x_12);
+lean_dec(x_3);
+x_54 = !lean_is_exclusive(x_47);
+if (x_54 == 0)
+{
+return x_47;
+}
+else
+{
+lean_object* x_55; lean_object* x_56; lean_object* x_57; 
+x_55 = lean_ctor_get(x_47, 0);
+x_56 = lean_ctor_get(x_47, 1);
+lean_inc(x_56);
+lean_inc(x_55);
+lean_dec(x_47);
+x_57 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_57, 0, x_55);
+lean_ctor_set(x_57, 1, x_56);
+return x_57;
+}
+}
+}
+else
+{
+uint8_t x_58; 
+lean_dec(x_40);
+lean_dec(x_15);
+lean_dec(x_12);
+lean_dec(x_3);
+x_58 = !lean_is_exclusive(x_44);
+if (x_58 == 0)
+{
+return x_44;
+}
+else
+{
+lean_object* x_59; lean_object* x_60; lean_object* x_61; 
+x_59 = lean_ctor_get(x_44, 0);
+x_60 = lean_ctor_get(x_44, 1);
+lean_inc(x_60);
+lean_inc(x_59);
+lean_dec(x_44);
+x_61 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_61, 0, x_59);
+lean_ctor_set(x_61, 1, x_60);
+return x_61;
+}
+}
+}
+}
+static lean_object* _init_l_mkRecOn___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string_unchecked("rec", 3, 3);
+return x_1;
+}
+}
+static lean_object* _init_l_mkRecOn___closed__2() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string_unchecked("", 0, 0);
+return x_1;
+}
+}
+static lean_object* _init_l_mkRecOn___closed__3() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_mkRecOn___closed__2;
+x_2 = l_Lean_stringToMessageData(x_1);
+return x_2;
+}
+}
+static lean_object* _init_l_mkRecOn___closed__4() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string_unchecked(" not a recinfo", 14, 14);
+return x_1;
+}
+}
+static lean_object* _init_l_mkRecOn___closed__5() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_mkRecOn___closed__4;
+x_2 = l_Lean_stringToMessageData(x_1);
+return x_2;
+}
+}
+static lean_object* _init_l_mkRecOn___closed__6() {
+_start:
+{
+lean_object* x_1; 
+x_1 = l_Lean_auxRecExt;
+return x_1;
+}
+}
+static lean_object* _init_l_mkRecOn___closed__7() {
+_start:
+{
+lean_object* x_1; 
+x_1 = l_Lean_protectedExt;
+return x_1;
+}
+}
+LEAN_EXPORT lean_object* l_mkRecOn(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
+_start:
+{
+lean_object* x_7; lean_object* x_8; lean_object* x_9; 
+x_7 = l_mkRecOn___closed__1;
+lean_inc(x_1);
+x_8 = l_Lean_Name_str___override(x_1, x_7);
+lean_inc(x_8);
+x_9 = l_Lean_getConstInfo___at_Lean_Meta_mkConstWithFreshMVarLevels___spec__1(x_8, x_2, x_3, x_4, x_5, x_6);
+if (lean_obj_tag(x_9) == 0)
+{
+lean_object* x_10; 
+x_10 = lean_ctor_get(x_9, 0);
+lean_inc(x_10);
+if (lean_obj_tag(x_10) == 7)
+{
+lean_object* x_11; uint8_t x_12; 
+lean_dec(x_8);
+x_11 = lean_ctor_get(x_9, 1);
+lean_inc(x_11);
+lean_dec(x_9);
+x_12 = !lean_is_exclusive(x_10);
+if (x_12 == 0)
+{
+lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; uint8_t x_17; lean_object* x_18; 
+x_13 = lean_ctor_get(x_10, 0);
+x_14 = lean_ctor_get(x_13, 0);
+lean_inc(x_14);
+x_15 = lean_ctor_get(x_14, 2);
+lean_inc(x_15);
+x_16 = lean_alloc_closure((void*)(l_mkRecOn___lambda__1___boxed), 10, 3);
+lean_closure_set(x_16, 0, x_14);
+lean_closure_set(x_16, 1, x_13);
+lean_closure_set(x_16, 2, x_1);
+x_17 = 0;
+lean_inc(x_5);
+lean_inc(x_4);
+lean_inc(x_3);
+lean_inc(x_2);
+x_18 = l_Lean_Meta_forallTelescope___at_Lean_Meta_mapForallTelescope_x27___spec__1___rarg(x_15, x_16, x_17, x_2, x_3, x_4, x_5, x_11);
+if (lean_obj_tag(x_18) == 0)
+{
+lean_object* x_19; lean_object* x_20; lean_object* x_21; 
+x_19 = lean_ctor_get(x_18, 0);
+lean_inc(x_19);
+x_20 = lean_ctor_get(x_18, 1);
+lean_inc(x_20);
+lean_dec(x_18);
+lean_inc(x_19);
+lean_ctor_set_tag(x_10, 1);
+lean_ctor_set(x_10, 0, x_19);
+lean_inc(x_5);
+lean_inc(x_4);
+x_21 = l_Lean_addDecl(x_10, x_4, x_5, x_20);
+if (lean_obj_tag(x_21) == 0)
+{
+lean_object* x_22; lean_object* x_23; lean_object* x_24; uint8_t x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; uint8_t x_31; 
+x_22 = lean_ctor_get(x_21, 1);
+lean_inc(x_22);
+lean_dec(x_21);
+x_23 = lean_ctor_get(x_19, 0);
+lean_inc(x_23);
+lean_dec(x_19);
+x_24 = lean_ctor_get(x_23, 0);
+lean_inc(x_24);
+lean_dec(x_23);
+x_25 = 0;
+lean_inc(x_24);
+x_26 = l_Lean_setReducibilityStatus___at_mkRecOn___spec__3(x_24, x_25, x_2, x_3, x_4, x_5, x_22);
+lean_dec(x_4);
+lean_dec(x_2);
+x_27 = lean_ctor_get(x_26, 1);
+lean_inc(x_27);
+lean_dec(x_26);
+x_28 = lean_st_ref_take(x_5, x_27);
+x_29 = lean_ctor_get(x_28, 0);
+lean_inc(x_29);
+x_30 = lean_ctor_get(x_28, 1);
+lean_inc(x_30);
+lean_dec(x_28);
+x_31 = !lean_is_exclusive(x_29);
+if (x_31 == 0)
+{
+lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; uint8_t x_42; 
+x_32 = lean_ctor_get(x_29, 0);
+x_33 = lean_ctor_get(x_29, 4);
+lean_dec(x_33);
+x_34 = l_mkRecOn___closed__6;
+lean_inc(x_24);
+x_35 = l_Lean_TagDeclarationExtension_tag(x_34, x_32, x_24);
+x_36 = l_Lean_setReducibilityStatus___at_mkRecOn___spec__3___closed__3;
+lean_ctor_set(x_29, 4, x_36);
+lean_ctor_set(x_29, 0, x_35);
+x_37 = lean_st_ref_set(x_5, x_29, x_30);
+x_38 = lean_ctor_get(x_37, 1);
+lean_inc(x_38);
+lean_dec(x_37);
+x_39 = lean_st_ref_take(x_3, x_38);
+x_40 = lean_ctor_get(x_39, 0);
+lean_inc(x_40);
+x_41 = lean_ctor_get(x_39, 1);
+lean_inc(x_41);
+lean_dec(x_39);
+x_42 = !lean_is_exclusive(x_40);
+if (x_42 == 0)
+{
+lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; uint8_t x_50; 
+x_43 = lean_ctor_get(x_40, 1);
+lean_dec(x_43);
+x_44 = l_Lean_setReducibilityStatus___at_mkRecOn___spec__3___closed__5;
+lean_ctor_set(x_40, 1, x_44);
+x_45 = lean_st_ref_set(x_3, x_40, x_41);
+x_46 = lean_ctor_get(x_45, 1);
+lean_inc(x_46);
+lean_dec(x_45);
+x_47 = lean_st_ref_take(x_5, x_46);
+x_48 = lean_ctor_get(x_47, 0);
+lean_inc(x_48);
+x_49 = lean_ctor_get(x_47, 1);
+lean_inc(x_49);
+lean_dec(x_47);
+x_50 = !lean_is_exclusive(x_48);
+if (x_50 == 0)
+{
+lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; uint8_t x_60; 
+x_51 = lean_ctor_get(x_48, 0);
+x_52 = lean_ctor_get(x_48, 4);
+lean_dec(x_52);
+x_53 = l_mkRecOn___closed__7;
+x_54 = l_Lean_TagDeclarationExtension_tag(x_53, x_51, x_24);
+lean_ctor_set(x_48, 4, x_36);
+lean_ctor_set(x_48, 0, x_54);
+x_55 = lean_st_ref_set(x_5, x_48, x_49);
+lean_dec(x_5);
+x_56 = lean_ctor_get(x_55, 1);
+lean_inc(x_56);
+lean_dec(x_55);
+x_57 = lean_st_ref_take(x_3, x_56);
+x_58 = lean_ctor_get(x_57, 0);
+lean_inc(x_58);
+x_59 = lean_ctor_get(x_57, 1);
+lean_inc(x_59);
+lean_dec(x_57);
+x_60 = !lean_is_exclusive(x_58);
+if (x_60 == 0)
+{
+lean_object* x_61; lean_object* x_62; uint8_t x_63; 
+x_61 = lean_ctor_get(x_58, 1);
+lean_dec(x_61);
+lean_ctor_set(x_58, 1, x_44);
+x_62 = lean_st_ref_set(x_3, x_58, x_59);
+lean_dec(x_3);
+x_63 = !lean_is_exclusive(x_62);
+if (x_63 == 0)
+{
+lean_object* x_64; lean_object* x_65; 
+x_64 = lean_ctor_get(x_62, 0);
+lean_dec(x_64);
+x_65 = lean_box(0);
+lean_ctor_set(x_62, 0, x_65);
+return x_62;
+}
+else
+{
+lean_object* x_66; lean_object* x_67; lean_object* x_68; 
+x_66 = lean_ctor_get(x_62, 1);
+lean_inc(x_66);
+lean_dec(x_62);
+x_67 = lean_box(0);
+x_68 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_68, 0, x_67);
+lean_ctor_set(x_68, 1, x_66);
+return x_68;
+}
+}
+else
+{
+lean_object* x_69; lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78; 
+x_69 = lean_ctor_get(x_58, 0);
+x_70 = lean_ctor_get(x_58, 2);
+x_71 = lean_ctor_get(x_58, 3);
+x_72 = lean_ctor_get(x_58, 4);
+lean_inc(x_72);
+lean_inc(x_71);
+lean_inc(x_70);
+lean_inc(x_69);
+lean_dec(x_58);
+x_73 = lean_alloc_ctor(0, 5, 0);
+lean_ctor_set(x_73, 0, x_69);
+lean_ctor_set(x_73, 1, x_44);
+lean_ctor_set(x_73, 2, x_70);
+lean_ctor_set(x_73, 3, x_71);
+lean_ctor_set(x_73, 4, x_72);
+x_74 = lean_st_ref_set(x_3, x_73, x_59);
+lean_dec(x_3);
+x_75 = lean_ctor_get(x_74, 1);
+lean_inc(x_75);
+if (lean_is_exclusive(x_74)) {
+ lean_ctor_release(x_74, 0);
+ lean_ctor_release(x_74, 1);
+ x_76 = x_74;
+} else {
+ lean_dec_ref(x_74);
+ x_76 = lean_box(0);
+}
+x_77 = lean_box(0);
+if (lean_is_scalar(x_76)) {
+ x_78 = lean_alloc_ctor(0, 2, 0);
+} else {
+ x_78 = x_76;
+}
+lean_ctor_set(x_78, 0, x_77);
+lean_ctor_set(x_78, 1, x_75);
+return x_78;
+}
+}
+else
+{
+lean_object* x_79; lean_object* x_80; lean_object* x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86; lean_object* x_87; lean_object* x_88; lean_object* x_89; lean_object* x_90; lean_object* x_91; lean_object* x_92; lean_object* x_93; lean_object* x_94; lean_object* x_95; lean_object* x_96; lean_object* x_97; lean_object* x_98; lean_object* x_99; lean_object* x_100; lean_object* x_101; lean_object* x_102; lean_object* x_103; 
+x_79 = lean_ctor_get(x_48, 0);
+x_80 = lean_ctor_get(x_48, 1);
+x_81 = lean_ctor_get(x_48, 2);
+x_82 = lean_ctor_get(x_48, 3);
+x_83 = lean_ctor_get(x_48, 5);
+x_84 = lean_ctor_get(x_48, 6);
+lean_inc(x_84);
+lean_inc(x_83);
+lean_inc(x_82);
+lean_inc(x_81);
+lean_inc(x_80);
+lean_inc(x_79);
+lean_dec(x_48);
+x_85 = l_mkRecOn___closed__7;
+x_86 = l_Lean_TagDeclarationExtension_tag(x_85, x_79, x_24);
+x_87 = lean_alloc_ctor(0, 7, 0);
+lean_ctor_set(x_87, 0, x_86);
+lean_ctor_set(x_87, 1, x_80);
+lean_ctor_set(x_87, 2, x_81);
+lean_ctor_set(x_87, 3, x_82);
+lean_ctor_set(x_87, 4, x_36);
+lean_ctor_set(x_87, 5, x_83);
+lean_ctor_set(x_87, 6, x_84);
+x_88 = lean_st_ref_set(x_5, x_87, x_49);
+lean_dec(x_5);
+x_89 = lean_ctor_get(x_88, 1);
+lean_inc(x_89);
+lean_dec(x_88);
+x_90 = lean_st_ref_take(x_3, x_89);
+x_91 = lean_ctor_get(x_90, 0);
+lean_inc(x_91);
+x_92 = lean_ctor_get(x_90, 1);
+lean_inc(x_92);
+lean_dec(x_90);
+x_93 = lean_ctor_get(x_91, 0);
+lean_inc(x_93);
+x_94 = lean_ctor_get(x_91, 2);
+lean_inc(x_94);
+x_95 = lean_ctor_get(x_91, 3);
+lean_inc(x_95);
+x_96 = lean_ctor_get(x_91, 4);
+lean_inc(x_96);
+if (lean_is_exclusive(x_91)) {
+ lean_ctor_release(x_91, 0);
+ lean_ctor_release(x_91, 1);
+ lean_ctor_release(x_91, 2);
+ lean_ctor_release(x_91, 3);
+ lean_ctor_release(x_91, 4);
+ x_97 = x_91;
+} else {
+ lean_dec_ref(x_91);
+ x_97 = lean_box(0);
+}
+if (lean_is_scalar(x_97)) {
+ x_98 = lean_alloc_ctor(0, 5, 0);
+} else {
+ x_98 = x_97;
+}
+lean_ctor_set(x_98, 0, x_93);
+lean_ctor_set(x_98, 1, x_44);
+lean_ctor_set(x_98, 2, x_94);
+lean_ctor_set(x_98, 3, x_95);
+lean_ctor_set(x_98, 4, x_96);
+x_99 = lean_st_ref_set(x_3, x_98, x_92);
+lean_dec(x_3);
+x_100 = lean_ctor_get(x_99, 1);
+lean_inc(x_100);
+if (lean_is_exclusive(x_99)) {
+ lean_ctor_release(x_99, 0);
+ lean_ctor_release(x_99, 1);
+ x_101 = x_99;
+} else {
+ lean_dec_ref(x_99);
+ x_101 = lean_box(0);
+}
+x_102 = lean_box(0);
+if (lean_is_scalar(x_101)) {
+ x_103 = lean_alloc_ctor(0, 2, 0);
+} else {
+ x_103 = x_101;
+}
+lean_ctor_set(x_103, 0, x_102);
+lean_ctor_set(x_103, 1, x_100);
+return x_103;
+}
+}
+else
+{
+lean_object* x_104; lean_object* x_105; lean_object* x_106; lean_object* x_107; lean_object* x_108; lean_object* x_109; lean_object* x_110; lean_object* x_111; lean_object* x_112; lean_object* x_113; lean_object* x_114; lean_object* x_115; lean_object* x_116; lean_object* x_117; lean_object* x_118; lean_object* x_119; lean_object* x_120; lean_object* x_121; lean_object* x_122; lean_object* x_123; lean_object* x_124; lean_object* x_125; lean_object* x_126; lean_object* x_127; lean_object* x_128; lean_object* x_129; lean_object* x_130; lean_object* x_131; lean_object* x_132; lean_object* x_133; lean_object* x_134; lean_object* x_135; lean_object* x_136; lean_object* x_137; lean_object* x_138; lean_object* x_139; lean_object* x_140; 
+x_104 = lean_ctor_get(x_40, 0);
+x_105 = lean_ctor_get(x_40, 2);
+x_106 = lean_ctor_get(x_40, 3);
+x_107 = lean_ctor_get(x_40, 4);
+lean_inc(x_107);
+lean_inc(x_106);
+lean_inc(x_105);
+lean_inc(x_104);
+lean_dec(x_40);
+x_108 = l_Lean_setReducibilityStatus___at_mkRecOn___spec__3___closed__5;
+x_109 = lean_alloc_ctor(0, 5, 0);
+lean_ctor_set(x_109, 0, x_104);
+lean_ctor_set(x_109, 1, x_108);
+lean_ctor_set(x_109, 2, x_105);
+lean_ctor_set(x_109, 3, x_106);
+lean_ctor_set(x_109, 4, x_107);
+x_110 = lean_st_ref_set(x_3, x_109, x_41);
+x_111 = lean_ctor_get(x_110, 1);
+lean_inc(x_111);
+lean_dec(x_110);
+x_112 = lean_st_ref_take(x_5, x_111);
+x_113 = lean_ctor_get(x_112, 0);
+lean_inc(x_113);
+x_114 = lean_ctor_get(x_112, 1);
+lean_inc(x_114);
+lean_dec(x_112);
+x_115 = lean_ctor_get(x_113, 0);
+lean_inc(x_115);
+x_116 = lean_ctor_get(x_113, 1);
+lean_inc(x_116);
+x_117 = lean_ctor_get(x_113, 2);
+lean_inc(x_117);
+x_118 = lean_ctor_get(x_113, 3);
+lean_inc(x_118);
+x_119 = lean_ctor_get(x_113, 5);
+lean_inc(x_119);
+x_120 = lean_ctor_get(x_113, 6);
+lean_inc(x_120);
+if (lean_is_exclusive(x_113)) {
+ lean_ctor_release(x_113, 0);
+ lean_ctor_release(x_113, 1);
+ lean_ctor_release(x_113, 2);
+ lean_ctor_release(x_113, 3);
+ lean_ctor_release(x_113, 4);
+ lean_ctor_release(x_113, 5);
+ lean_ctor_release(x_113, 6);
+ x_121 = x_113;
+} else {
+ lean_dec_ref(x_113);
+ x_121 = lean_box(0);
+}
+x_122 = l_mkRecOn___closed__7;
+x_123 = l_Lean_TagDeclarationExtension_tag(x_122, x_115, x_24);
+if (lean_is_scalar(x_121)) {
+ x_124 = lean_alloc_ctor(0, 7, 0);
+} else {
+ x_124 = x_121;
+}
+lean_ctor_set(x_124, 0, x_123);
+lean_ctor_set(x_124, 1, x_116);
+lean_ctor_set(x_124, 2, x_117);
+lean_ctor_set(x_124, 3, x_118);
+lean_ctor_set(x_124, 4, x_36);
+lean_ctor_set(x_124, 5, x_119);
+lean_ctor_set(x_124, 6, x_120);
+x_125 = lean_st_ref_set(x_5, x_124, x_114);
+lean_dec(x_5);
+x_126 = lean_ctor_get(x_125, 1);
+lean_inc(x_126);
+lean_dec(x_125);
+x_127 = lean_st_ref_take(x_3, x_126);
+x_128 = lean_ctor_get(x_127, 0);
+lean_inc(x_128);
+x_129 = lean_ctor_get(x_127, 1);
+lean_inc(x_129);
+lean_dec(x_127);
+x_130 = lean_ctor_get(x_128, 0);
+lean_inc(x_130);
+x_131 = lean_ctor_get(x_128, 2);
+lean_inc(x_131);
+x_132 = lean_ctor_get(x_128, 3);
+lean_inc(x_132);
+x_133 = lean_ctor_get(x_128, 4);
+lean_inc(x_133);
+if (lean_is_exclusive(x_128)) {
+ lean_ctor_release(x_128, 0);
+ lean_ctor_release(x_128, 1);
+ lean_ctor_release(x_128, 2);
+ lean_ctor_release(x_128, 3);
+ lean_ctor_release(x_128, 4);
+ x_134 = x_128;
+} else {
+ lean_dec_ref(x_128);
+ x_134 = lean_box(0);
+}
+if (lean_is_scalar(x_134)) {
+ x_135 = lean_alloc_ctor(0, 5, 0);
+} else {
+ x_135 = x_134;
+}
+lean_ctor_set(x_135, 0, x_130);
+lean_ctor_set(x_135, 1, x_108);
+lean_ctor_set(x_135, 2, x_131);
+lean_ctor_set(x_135, 3, x_132);
+lean_ctor_set(x_135, 4, x_133);
+x_136 = lean_st_ref_set(x_3, x_135, x_129);
+lean_dec(x_3);
+x_137 = lean_ctor_get(x_136, 1);
+lean_inc(x_137);
+if (lean_is_exclusive(x_136)) {
+ lean_ctor_release(x_136, 0);
+ lean_ctor_release(x_136, 1);
+ x_138 = x_136;
+} else {
+ lean_dec_ref(x_136);
+ x_138 = lean_box(0);
+}
+x_139 = lean_box(0);
+if (lean_is_scalar(x_138)) {
+ x_140 = lean_alloc_ctor(0, 2, 0);
+} else {
+ x_140 = x_138;
+}
+lean_ctor_set(x_140, 0, x_139);
+lean_ctor_set(x_140, 1, x_137);
+return x_140;
+}
+}
+else
+{
+lean_object* x_141; lean_object* x_142; lean_object* x_143; lean_object* x_144; lean_object* x_145; lean_object* x_146; lean_object* x_147; lean_object* x_148; lean_object* x_149; lean_object* x_150; lean_object* x_151; lean_object* x_152; lean_object* x_153; lean_object* x_154; lean_object* x_155; lean_object* x_156; lean_object* x_157; lean_object* x_158; lean_object* x_159; lean_object* x_160; lean_object* x_161; lean_object* x_162; lean_object* x_163; lean_object* x_164; lean_object* x_165; lean_object* x_166; lean_object* x_167; lean_object* x_168; lean_object* x_169; lean_object* x_170; lean_object* x_171; lean_object* x_172; lean_object* x_173; lean_object* x_174; lean_object* x_175; lean_object* x_176; lean_object* x_177; lean_object* x_178; lean_object* x_179; lean_object* x_180; lean_object* x_181; lean_object* x_182; lean_object* x_183; lean_object* x_184; lean_object* x_185; lean_object* x_186; lean_object* x_187; lean_object* x_188; lean_object* x_189; lean_object* x_190; lean_object* x_191; lean_object* x_192; lean_object* x_193; 
+x_141 = lean_ctor_get(x_29, 0);
+x_142 = lean_ctor_get(x_29, 1);
+x_143 = lean_ctor_get(x_29, 2);
+x_144 = lean_ctor_get(x_29, 3);
+x_145 = lean_ctor_get(x_29, 5);
+x_146 = lean_ctor_get(x_29, 6);
+lean_inc(x_146);
+lean_inc(x_145);
+lean_inc(x_144);
+lean_inc(x_143);
+lean_inc(x_142);
+lean_inc(x_141);
+lean_dec(x_29);
+x_147 = l_mkRecOn___closed__6;
+lean_inc(x_24);
+x_148 = l_Lean_TagDeclarationExtension_tag(x_147, x_141, x_24);
+x_149 = l_Lean_setReducibilityStatus___at_mkRecOn___spec__3___closed__3;
+x_150 = lean_alloc_ctor(0, 7, 0);
+lean_ctor_set(x_150, 0, x_148);
+lean_ctor_set(x_150, 1, x_142);
+lean_ctor_set(x_150, 2, x_143);
+lean_ctor_set(x_150, 3, x_144);
+lean_ctor_set(x_150, 4, x_149);
+lean_ctor_set(x_150, 5, x_145);
+lean_ctor_set(x_150, 6, x_146);
+x_151 = lean_st_ref_set(x_5, x_150, x_30);
+x_152 = lean_ctor_get(x_151, 1);
+lean_inc(x_152);
+lean_dec(x_151);
+x_153 = lean_st_ref_take(x_3, x_152);
+x_154 = lean_ctor_get(x_153, 0);
+lean_inc(x_154);
+x_155 = lean_ctor_get(x_153, 1);
+lean_inc(x_155);
+lean_dec(x_153);
+x_156 = lean_ctor_get(x_154, 0);
+lean_inc(x_156);
+x_157 = lean_ctor_get(x_154, 2);
+lean_inc(x_157);
+x_158 = lean_ctor_get(x_154, 3);
+lean_inc(x_158);
+x_159 = lean_ctor_get(x_154, 4);
+lean_inc(x_159);
+if (lean_is_exclusive(x_154)) {
+ lean_ctor_release(x_154, 0);
+ lean_ctor_release(x_154, 1);
+ lean_ctor_release(x_154, 2);
+ lean_ctor_release(x_154, 3);
+ lean_ctor_release(x_154, 4);
+ x_160 = x_154;
+} else {
+ lean_dec_ref(x_154);
+ x_160 = lean_box(0);
+}
+x_161 = l_Lean_setReducibilityStatus___at_mkRecOn___spec__3___closed__5;
+if (lean_is_scalar(x_160)) {
+ x_162 = lean_alloc_ctor(0, 5, 0);
+} else {
+ x_162 = x_160;
+}
+lean_ctor_set(x_162, 0, x_156);
+lean_ctor_set(x_162, 1, x_161);
+lean_ctor_set(x_162, 2, x_157);
+lean_ctor_set(x_162, 3, x_158);
+lean_ctor_set(x_162, 4, x_159);
+x_163 = lean_st_ref_set(x_3, x_162, x_155);
+x_164 = lean_ctor_get(x_163, 1);
+lean_inc(x_164);
+lean_dec(x_163);
+x_165 = lean_st_ref_take(x_5, x_164);
+x_166 = lean_ctor_get(x_165, 0);
+lean_inc(x_166);
+x_167 = lean_ctor_get(x_165, 1);
+lean_inc(x_167);
+lean_dec(x_165);
+x_168 = lean_ctor_get(x_166, 0);
+lean_inc(x_168);
+x_169 = lean_ctor_get(x_166, 1);
+lean_inc(x_169);
+x_170 = lean_ctor_get(x_166, 2);
+lean_inc(x_170);
+x_171 = lean_ctor_get(x_166, 3);
+lean_inc(x_171);
+x_172 = lean_ctor_get(x_166, 5);
+lean_inc(x_172);
+x_173 = lean_ctor_get(x_166, 6);
+lean_inc(x_173);
+if (lean_is_exclusive(x_166)) {
+ lean_ctor_release(x_166, 0);
+ lean_ctor_release(x_166, 1);
+ lean_ctor_release(x_166, 2);
+ lean_ctor_release(x_166, 3);
+ lean_ctor_release(x_166, 4);
+ lean_ctor_release(x_166, 5);
+ lean_ctor_release(x_166, 6);
+ x_174 = x_166;
+} else {
+ lean_dec_ref(x_166);
+ x_174 = lean_box(0);
+}
+x_175 = l_mkRecOn___closed__7;
+x_176 = l_Lean_TagDeclarationExtension_tag(x_175, x_168, x_24);
+if (lean_is_scalar(x_174)) {
+ x_177 = lean_alloc_ctor(0, 7, 0);
+} else {
+ x_177 = x_174;
+}
+lean_ctor_set(x_177, 0, x_176);
+lean_ctor_set(x_177, 1, x_169);
+lean_ctor_set(x_177, 2, x_170);
+lean_ctor_set(x_177, 3, x_171);
+lean_ctor_set(x_177, 4, x_149);
+lean_ctor_set(x_177, 5, x_172);
+lean_ctor_set(x_177, 6, x_173);
+x_178 = lean_st_ref_set(x_5, x_177, x_167);
+lean_dec(x_5);
+x_179 = lean_ctor_get(x_178, 1);
+lean_inc(x_179);
+lean_dec(x_178);
+x_180 = lean_st_ref_take(x_3, x_179);
+x_181 = lean_ctor_get(x_180, 0);
+lean_inc(x_181);
+x_182 = lean_ctor_get(x_180, 1);
+lean_inc(x_182);
+lean_dec(x_180);
+x_183 = lean_ctor_get(x_181, 0);
+lean_inc(x_183);
+x_184 = lean_ctor_get(x_181, 2);
+lean_inc(x_184);
+x_185 = lean_ctor_get(x_181, 3);
+lean_inc(x_185);
+x_186 = lean_ctor_get(x_181, 4);
+lean_inc(x_186);
+if (lean_is_exclusive(x_181)) {
+ lean_ctor_release(x_181, 0);
+ lean_ctor_release(x_181, 1);
+ lean_ctor_release(x_181, 2);
+ lean_ctor_release(x_181, 3);
+ lean_ctor_release(x_181, 4);
+ x_187 = x_181;
+} else {
+ lean_dec_ref(x_181);
+ x_187 = lean_box(0);
+}
+if (lean_is_scalar(x_187)) {
+ x_188 = lean_alloc_ctor(0, 5, 0);
+} else {
+ x_188 = x_187;
+}
+lean_ctor_set(x_188, 0, x_183);
+lean_ctor_set(x_188, 1, x_161);
+lean_ctor_set(x_188, 2, x_184);
+lean_ctor_set(x_188, 3, x_185);
+lean_ctor_set(x_188, 4, x_186);
+x_189 = lean_st_ref_set(x_3, x_188, x_182);
+lean_dec(x_3);
+x_190 = lean_ctor_get(x_189, 1);
+lean_inc(x_190);
+if (lean_is_exclusive(x_189)) {
+ lean_ctor_release(x_189, 0);
+ lean_ctor_release(x_189, 1);
+ x_191 = x_189;
+} else {
+ lean_dec_ref(x_189);
+ x_191 = lean_box(0);
+}
+x_192 = lean_box(0);
+if (lean_is_scalar(x_191)) {
+ x_193 = lean_alloc_ctor(0, 2, 0);
+} else {
+ x_193 = x_191;
+}
+lean_ctor_set(x_193, 0, x_192);
+lean_ctor_set(x_193, 1, x_190);
+return x_193;
+}
+}
+else
+{
+uint8_t x_194; 
+lean_dec(x_19);
+lean_dec(x_5);
+lean_dec(x_4);
+lean_dec(x_3);
+lean_dec(x_2);
+x_194 = !lean_is_exclusive(x_21);
+if (x_194 == 0)
+{
+return x_21;
+}
+else
+{
+lean_object* x_195; lean_object* x_196; lean_object* x_197; 
+x_195 = lean_ctor_get(x_21, 0);
+x_196 = lean_ctor_get(x_21, 1);
+lean_inc(x_196);
+lean_inc(x_195);
+lean_dec(x_21);
+x_197 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_197, 0, x_195);
+lean_ctor_set(x_197, 1, x_196);
+return x_197;
+}
+}
+}
+else
+{
+uint8_t x_198; 
+lean_free_object(x_10);
+lean_dec(x_5);
+lean_dec(x_4);
+lean_dec(x_3);
+lean_dec(x_2);
+x_198 = !lean_is_exclusive(x_18);
+if (x_198 == 0)
+{
+return x_18;
+}
+else
+{
+lean_object* x_199; lean_object* x_200; lean_object* x_201; 
+x_199 = lean_ctor_get(x_18, 0);
+x_200 = lean_ctor_get(x_18, 1);
+lean_inc(x_200);
+lean_inc(x_199);
+lean_dec(x_18);
+x_201 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_201, 0, x_199);
+lean_ctor_set(x_201, 1, x_200);
+return x_201;
+}
+}
+}
+else
+{
+lean_object* x_202; lean_object* x_203; lean_object* x_204; lean_object* x_205; uint8_t x_206; lean_object* x_207; 
+x_202 = lean_ctor_get(x_10, 0);
+lean_inc(x_202);
+lean_dec(x_10);
+x_203 = lean_ctor_get(x_202, 0);
+lean_inc(x_203);
+x_204 = lean_ctor_get(x_203, 2);
+lean_inc(x_204);
+x_205 = lean_alloc_closure((void*)(l_mkRecOn___lambda__1___boxed), 10, 3);
+lean_closure_set(x_205, 0, x_203);
+lean_closure_set(x_205, 1, x_202);
+lean_closure_set(x_205, 2, x_1);
+x_206 = 0;
+lean_inc(x_5);
+lean_inc(x_4);
+lean_inc(x_3);
+lean_inc(x_2);
+x_207 = l_Lean_Meta_forallTelescope___at_Lean_Meta_mapForallTelescope_x27___spec__1___rarg(x_204, x_205, x_206, x_2, x_3, x_4, x_5, x_11);
+if (lean_obj_tag(x_207) == 0)
+{
+lean_object* x_208; lean_object* x_209; lean_object* x_210; lean_object* x_211; 
+x_208 = lean_ctor_get(x_207, 0);
+lean_inc(x_208);
+x_209 = lean_ctor_get(x_207, 1);
+lean_inc(x_209);
+lean_dec(x_207);
+lean_inc(x_208);
+x_210 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_210, 0, x_208);
+lean_inc(x_5);
+lean_inc(x_4);
+x_211 = l_Lean_addDecl(x_210, x_4, x_5, x_209);
+if (lean_obj_tag(x_211) == 0)
+{
+lean_object* x_212; lean_object* x_213; lean_object* x_214; uint8_t x_215; lean_object* x_216; lean_object* x_217; lean_object* x_218; lean_object* x_219; lean_object* x_220; lean_object* x_221; lean_object* x_222; lean_object* x_223; lean_object* x_224; lean_object* x_225; lean_object* x_226; lean_object* x_227; lean_object* x_228; lean_object* x_229; lean_object* x_230; lean_object* x_231; lean_object* x_232; lean_object* x_233; lean_object* x_234; lean_object* x_235; lean_object* x_236; lean_object* x_237; lean_object* x_238; lean_object* x_239; lean_object* x_240; lean_object* x_241; lean_object* x_242; lean_object* x_243; lean_object* x_244; lean_object* x_245; lean_object* x_246; lean_object* x_247; lean_object* x_248; lean_object* x_249; lean_object* x_250; lean_object* x_251; lean_object* x_252; lean_object* x_253; lean_object* x_254; lean_object* x_255; lean_object* x_256; lean_object* x_257; lean_object* x_258; lean_object* x_259; lean_object* x_260; lean_object* x_261; lean_object* x_262; lean_object* x_263; lean_object* x_264; lean_object* x_265; lean_object* x_266; lean_object* x_267; lean_object* x_268; lean_object* x_269; lean_object* x_270; lean_object* x_271; lean_object* x_272; lean_object* x_273; lean_object* x_274; 
+x_212 = lean_ctor_get(x_211, 1);
+lean_inc(x_212);
+lean_dec(x_211);
+x_213 = lean_ctor_get(x_208, 0);
+lean_inc(x_213);
+lean_dec(x_208);
+x_214 = lean_ctor_get(x_213, 0);
+lean_inc(x_214);
+lean_dec(x_213);
+x_215 = 0;
+lean_inc(x_214);
+x_216 = l_Lean_setReducibilityStatus___at_mkRecOn___spec__3(x_214, x_215, x_2, x_3, x_4, x_5, x_212);
+lean_dec(x_4);
+lean_dec(x_2);
+x_217 = lean_ctor_get(x_216, 1);
+lean_inc(x_217);
+lean_dec(x_216);
+x_218 = lean_st_ref_take(x_5, x_217);
+x_219 = lean_ctor_get(x_218, 0);
+lean_inc(x_219);
+x_220 = lean_ctor_get(x_218, 1);
+lean_inc(x_220);
+lean_dec(x_218);
+x_221 = lean_ctor_get(x_219, 0);
+lean_inc(x_221);
+x_222 = lean_ctor_get(x_219, 1);
+lean_inc(x_222);
+x_223 = lean_ctor_get(x_219, 2);
+lean_inc(x_223);
+x_224 = lean_ctor_get(x_219, 3);
+lean_inc(x_224);
+x_225 = lean_ctor_get(x_219, 5);
+lean_inc(x_225);
+x_226 = lean_ctor_get(x_219, 6);
+lean_inc(x_226);
+if (lean_is_exclusive(x_219)) {
+ lean_ctor_release(x_219, 0);
+ lean_ctor_release(x_219, 1);
+ lean_ctor_release(x_219, 2);
+ lean_ctor_release(x_219, 3);
+ lean_ctor_release(x_219, 4);
+ lean_ctor_release(x_219, 5);
+ lean_ctor_release(x_219, 6);
+ x_227 = x_219;
+} else {
+ lean_dec_ref(x_219);
+ x_227 = lean_box(0);
+}
+x_228 = l_mkRecOn___closed__6;
+lean_inc(x_214);
+x_229 = l_Lean_TagDeclarationExtension_tag(x_228, x_221, x_214);
+x_230 = l_Lean_setReducibilityStatus___at_mkRecOn___spec__3___closed__3;
+if (lean_is_scalar(x_227)) {
+ x_231 = lean_alloc_ctor(0, 7, 0);
+} else {
+ x_231 = x_227;
+}
+lean_ctor_set(x_231, 0, x_229);
+lean_ctor_set(x_231, 1, x_222);
+lean_ctor_set(x_231, 2, x_223);
+lean_ctor_set(x_231, 3, x_224);
+lean_ctor_set(x_231, 4, x_230);
+lean_ctor_set(x_231, 5, x_225);
+lean_ctor_set(x_231, 6, x_226);
+x_232 = lean_st_ref_set(x_5, x_231, x_220);
+x_233 = lean_ctor_get(x_232, 1);
+lean_inc(x_233);
+lean_dec(x_232);
+x_234 = lean_st_ref_take(x_3, x_233);
+x_235 = lean_ctor_get(x_234, 0);
+lean_inc(x_235);
+x_236 = lean_ctor_get(x_234, 1);
+lean_inc(x_236);
+lean_dec(x_234);
+x_237 = lean_ctor_get(x_235, 0);
+lean_inc(x_237);
+x_238 = lean_ctor_get(x_235, 2);
+lean_inc(x_238);
+x_239 = lean_ctor_get(x_235, 3);
+lean_inc(x_239);
+x_240 = lean_ctor_get(x_235, 4);
+lean_inc(x_240);
+if (lean_is_exclusive(x_235)) {
+ lean_ctor_release(x_235, 0);
+ lean_ctor_release(x_235, 1);
+ lean_ctor_release(x_235, 2);
+ lean_ctor_release(x_235, 3);
+ lean_ctor_release(x_235, 4);
+ x_241 = x_235;
+} else {
+ lean_dec_ref(x_235);
+ x_241 = lean_box(0);
+}
+x_242 = l_Lean_setReducibilityStatus___at_mkRecOn___spec__3___closed__5;
+if (lean_is_scalar(x_241)) {
+ x_243 = lean_alloc_ctor(0, 5, 0);
+} else {
+ x_243 = x_241;
+}
+lean_ctor_set(x_243, 0, x_237);
+lean_ctor_set(x_243, 1, x_242);
+lean_ctor_set(x_243, 2, x_238);
+lean_ctor_set(x_243, 3, x_239);
+lean_ctor_set(x_243, 4, x_240);
+x_244 = lean_st_ref_set(x_3, x_243, x_236);
+x_245 = lean_ctor_get(x_244, 1);
+lean_inc(x_245);
+lean_dec(x_244);
+x_246 = lean_st_ref_take(x_5, x_245);
+x_247 = lean_ctor_get(x_246, 0);
+lean_inc(x_247);
+x_248 = lean_ctor_get(x_246, 1);
+lean_inc(x_248);
+lean_dec(x_246);
+x_249 = lean_ctor_get(x_247, 0);
+lean_inc(x_249);
+x_250 = lean_ctor_get(x_247, 1);
+lean_inc(x_250);
+x_251 = lean_ctor_get(x_247, 2);
+lean_inc(x_251);
+x_252 = lean_ctor_get(x_247, 3);
+lean_inc(x_252);
+x_253 = lean_ctor_get(x_247, 5);
+lean_inc(x_253);
+x_254 = lean_ctor_get(x_247, 6);
+lean_inc(x_254);
+if (lean_is_exclusive(x_247)) {
+ lean_ctor_release(x_247, 0);
+ lean_ctor_release(x_247, 1);
+ lean_ctor_release(x_247, 2);
+ lean_ctor_release(x_247, 3);
+ lean_ctor_release(x_247, 4);
+ lean_ctor_release(x_247, 5);
+ lean_ctor_release(x_247, 6);
+ x_255 = x_247;
+} else {
+ lean_dec_ref(x_247);
+ x_255 = lean_box(0);
+}
+x_256 = l_mkRecOn___closed__7;
+x_257 = l_Lean_TagDeclarationExtension_tag(x_256, x_249, x_214);
+if (lean_is_scalar(x_255)) {
+ x_258 = lean_alloc_ctor(0, 7, 0);
+} else {
+ x_258 = x_255;
+}
+lean_ctor_set(x_258, 0, x_257);
+lean_ctor_set(x_258, 1, x_250);
+lean_ctor_set(x_258, 2, x_251);
+lean_ctor_set(x_258, 3, x_252);
+lean_ctor_set(x_258, 4, x_230);
+lean_ctor_set(x_258, 5, x_253);
+lean_ctor_set(x_258, 6, x_254);
+x_259 = lean_st_ref_set(x_5, x_258, x_248);
+lean_dec(x_5);
+x_260 = lean_ctor_get(x_259, 1);
+lean_inc(x_260);
+lean_dec(x_259);
+x_261 = lean_st_ref_take(x_3, x_260);
+x_262 = lean_ctor_get(x_261, 0);
+lean_inc(x_262);
+x_263 = lean_ctor_get(x_261, 1);
+lean_inc(x_263);
+lean_dec(x_261);
+x_264 = lean_ctor_get(x_262, 0);
+lean_inc(x_264);
+x_265 = lean_ctor_get(x_262, 2);
+lean_inc(x_265);
+x_266 = lean_ctor_get(x_262, 3);
+lean_inc(x_266);
+x_267 = lean_ctor_get(x_262, 4);
+lean_inc(x_267);
+if (lean_is_exclusive(x_262)) {
+ lean_ctor_release(x_262, 0);
+ lean_ctor_release(x_262, 1);
+ lean_ctor_release(x_262, 2);
+ lean_ctor_release(x_262, 3);
+ lean_ctor_release(x_262, 4);
+ x_268 = x_262;
+} else {
+ lean_dec_ref(x_262);
+ x_268 = lean_box(0);
+}
+if (lean_is_scalar(x_268)) {
+ x_269 = lean_alloc_ctor(0, 5, 0);
+} else {
+ x_269 = x_268;
+}
+lean_ctor_set(x_269, 0, x_264);
+lean_ctor_set(x_269, 1, x_242);
+lean_ctor_set(x_269, 2, x_265);
+lean_ctor_set(x_269, 3, x_266);
+lean_ctor_set(x_269, 4, x_267);
+x_270 = lean_st_ref_set(x_3, x_269, x_263);
+lean_dec(x_3);
+x_271 = lean_ctor_get(x_270, 1);
+lean_inc(x_271);
+if (lean_is_exclusive(x_270)) {
+ lean_ctor_release(x_270, 0);
+ lean_ctor_release(x_270, 1);
+ x_272 = x_270;
+} else {
+ lean_dec_ref(x_270);
+ x_272 = lean_box(0);
+}
+x_273 = lean_box(0);
+if (lean_is_scalar(x_272)) {
+ x_274 = lean_alloc_ctor(0, 2, 0);
+} else {
+ x_274 = x_272;
+}
+lean_ctor_set(x_274, 0, x_273);
+lean_ctor_set(x_274, 1, x_271);
+return x_274;
+}
+else
+{
+lean_object* x_275; lean_object* x_276; lean_object* x_277; lean_object* x_278; 
+lean_dec(x_208);
+lean_dec(x_5);
+lean_dec(x_4);
+lean_dec(x_3);
+lean_dec(x_2);
+x_275 = lean_ctor_get(x_211, 0);
+lean_inc(x_275);
+x_276 = lean_ctor_get(x_211, 1);
+lean_inc(x_276);
+if (lean_is_exclusive(x_211)) {
+ lean_ctor_release(x_211, 0);
+ lean_ctor_release(x_211, 1);
+ x_277 = x_211;
+} else {
+ lean_dec_ref(x_211);
+ x_277 = lean_box(0);
+}
+if (lean_is_scalar(x_277)) {
+ x_278 = lean_alloc_ctor(1, 2, 0);
+} else {
+ x_278 = x_277;
+}
+lean_ctor_set(x_278, 0, x_275);
+lean_ctor_set(x_278, 1, x_276);
+return x_278;
+}
+}
+else
+{
+lean_object* x_279; lean_object* x_280; lean_object* x_281; lean_object* x_282; 
+lean_dec(x_5);
+lean_dec(x_4);
+lean_dec(x_3);
+lean_dec(x_2);
+x_279 = lean_ctor_get(x_207, 0);
+lean_inc(x_279);
+x_280 = lean_ctor_get(x_207, 1);
+lean_inc(x_280);
+if (lean_is_exclusive(x_207)) {
+ lean_ctor_release(x_207, 0);
+ lean_ctor_release(x_207, 1);
+ x_281 = x_207;
+} else {
+ lean_dec_ref(x_207);
+ x_281 = lean_box(0);
+}
+if (lean_is_scalar(x_281)) {
+ x_282 = lean_alloc_ctor(1, 2, 0);
+} else {
+ x_282 = x_281;
+}
+lean_ctor_set(x_282, 0, x_279);
+lean_ctor_set(x_282, 1, x_280);
+return x_282;
+}
+}
+}
+else
+{
+lean_object* x_283; lean_object* x_284; lean_object* x_285; lean_object* x_286; lean_object* x_287; lean_object* x_288; lean_object* x_289; 
+lean_dec(x_10);
+lean_dec(x_1);
+x_283 = lean_ctor_get(x_9, 1);
+lean_inc(x_283);
+lean_dec(x_9);
+x_284 = l_Lean_MessageData_ofName(x_8);
+x_285 = l_mkRecOn___closed__3;
+x_286 = lean_alloc_ctor(7, 2, 0);
+lean_ctor_set(x_286, 0, x_285);
+lean_ctor_set(x_286, 1, x_284);
+x_287 = l_mkRecOn___closed__5;
+x_288 = lean_alloc_ctor(7, 2, 0);
+lean_ctor_set(x_288, 0, x_286);
+lean_ctor_set(x_288, 1, x_287);
+x_289 = l_Lean_throwError___at_Lean_Meta_setInlineAttribute___spec__1(x_288, x_2, x_3, x_4, x_5, x_283);
+lean_dec(x_5);
+lean_dec(x_4);
+lean_dec(x_3);
+lean_dec(x_2);
+return x_289;
+}
+}
+else
+{
+uint8_t x_290; 
+lean_dec(x_8);
+lean_dec(x_5);
+lean_dec(x_4);
+lean_dec(x_3);
+lean_dec(x_2);
+lean_dec(x_1);
+x_290 = !lean_is_exclusive(x_9);
+if (x_290 == 0)
+{
+return x_9;
+}
+else
+{
+lean_object* x_291; lean_object* x_292; lean_object* x_293; 
+x_291 = lean_ctor_get(x_9, 0);
+x_292 = lean_ctor_get(x_9, 1);
+lean_inc(x_292);
+lean_inc(x_291);
+lean_dec(x_9);
+x_293 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_293, 0, x_291);
+lean_ctor_set(x_293, 1, x_292);
+return x_293;
+}
+}
+}
+}
+LEAN_EXPORT lean_object* l_Lean_mkDefinitionValInferrringUnsafe___at_mkRecOn___spec__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
+_start:
+{
+lean_object* x_11; 
+x_11 = l_Lean_mkDefinitionValInferrringUnsafe___at_mkRecOn___spec__2(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
+lean_dec(x_9);
+lean_dec(x_8);
+lean_dec(x_7);
+lean_dec(x_6);
+return x_11;
+}
+}
+LEAN_EXPORT lean_object* l_Lean_setReducibilityStatus___at_mkRecOn___spec__3___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
+_start:
+{
+uint8_t x_8; lean_object* x_9; 
+x_8 = lean_unbox(x_2);
+lean_dec(x_2);
+x_9 = l_Lean_setReducibilityStatus___at_mkRecOn___spec__3(x_1, x_8, x_3, x_4, x_5, x_6, x_7);
+lean_dec(x_6);
+lean_dec(x_5);
+lean_dec(x_4);
+lean_dec(x_3);
+return x_9;
+}
+}
+LEAN_EXPORT lean_object* l_mkRecOn___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
+_start:
+{
+lean_object* x_11; 
+x_11 = l_mkRecOn___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
+lean_dec(x_9);
+lean_dec(x_8);
+lean_dec(x_7);
+lean_dec(x_6);
+lean_dec(x_2);
+return x_11;
+}
+}
+lean_object* initialize_Lean_Meta_InferType(uint8_t builtin, lean_object*);
+lean_object* initialize_Lean_AuxRecursor(uint8_t builtin, lean_object*);
+lean_object* initialize_Lean_AddDecl(uint8_t builtin, lean_object*);
+lean_object* initialize_Lean_Meta_CompletionName(uint8_t builtin, lean_object*);
+static bool _G_initialized = false;
+LEAN_EXPORT lean_object* initialize_Lean_Meta_Constructions_RecOn(uint8_t builtin, lean_object* w) {
+lean_object * res;
+if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
+_G_initialized = true;
+res = initialize_Lean_Meta_InferType(builtin, lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+res = initialize_Lean_AuxRecursor(builtin, lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+res = initialize_Lean_AddDecl(builtin, lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+res = initialize_Lean_Meta_CompletionName(builtin, lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+l_Lean_setReducibilityStatus___at_mkRecOn___spec__3___closed__1 = _init_l_Lean_setReducibilityStatus___at_mkRecOn___spec__3___closed__1();
+lean_mark_persistent(l_Lean_setReducibilityStatus___at_mkRecOn___spec__3___closed__1);
+l_Lean_setReducibilityStatus___at_mkRecOn___spec__3___closed__2 = _init_l_Lean_setReducibilityStatus___at_mkRecOn___spec__3___closed__2();
+lean_mark_persistent(l_Lean_setReducibilityStatus___at_mkRecOn___spec__3___closed__2);
+l_Lean_setReducibilityStatus___at_mkRecOn___spec__3___closed__3 = _init_l_Lean_setReducibilityStatus___at_mkRecOn___spec__3___closed__3();
+lean_mark_persistent(l_Lean_setReducibilityStatus___at_mkRecOn___spec__3___closed__3);
+l_Lean_setReducibilityStatus___at_mkRecOn___spec__3___closed__4 = _init_l_Lean_setReducibilityStatus___at_mkRecOn___spec__3___closed__4();
+lean_mark_persistent(l_Lean_setReducibilityStatus___at_mkRecOn___spec__3___closed__4);
+l_Lean_setReducibilityStatus___at_mkRecOn___spec__3___closed__5 = _init_l_Lean_setReducibilityStatus___at_mkRecOn___spec__3___closed__5();
+lean_mark_persistent(l_Lean_setReducibilityStatus___at_mkRecOn___spec__3___closed__5);
+l_mkRecOn___closed__1 = _init_l_mkRecOn___closed__1();
+lean_mark_persistent(l_mkRecOn___closed__1);
+l_mkRecOn___closed__2 = _init_l_mkRecOn___closed__2();
+lean_mark_persistent(l_mkRecOn___closed__2);
+l_mkRecOn___closed__3 = _init_l_mkRecOn___closed__3();
+lean_mark_persistent(l_mkRecOn___closed__3);
+l_mkRecOn___closed__4 = _init_l_mkRecOn___closed__4();
+lean_mark_persistent(l_mkRecOn___closed__4);
+l_mkRecOn___closed__5 = _init_l_mkRecOn___closed__5();
+lean_mark_persistent(l_mkRecOn___closed__5);
+l_mkRecOn___closed__6 = _init_l_mkRecOn___closed__6();
+lean_mark_persistent(l_mkRecOn___closed__6);
+l_mkRecOn___closed__7 = _init_l_mkRecOn___closed__7();
+lean_mark_persistent(l_mkRecOn___closed__7);
+return lean_io_result_mk_ok(lean_box(0));
+}
+#ifdef __cplusplus
+}
+#endif