From 45dc2cd49a16392c0d6c412febafebffe052dce7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 24 Jun 2019 14:23:35 -0700
Subject: [PATCH] feat(library/init/lean/compiler): `[export]` attribute in
 Lean

---
 library/init/lean/compiler/export.lean       |   15 -
 library/init/lean/compiler/exportattr.lean   |   38 +
 library/init/lean/compiler/ir/borrow.lean    |    2 +-
 library/init/lean/compiler/ir/emitcpp.lean   |    2 +-
 src/library/compiler/export_attribute.cpp    |   55 +-
 src/library/compiler/export_attribute.h      |    2 -
 src/library/compiler/init_module.cpp         |    3 -
 src/stage0/CMakeLists.txt                    |    2 +-
 src/stage0/init/core.cpp                     |   26 +-
 src/stage0/init/lean/compiler/export.cpp     |   71 -
 src/stage0/init/lean/compiler/exportattr.cpp | 1303 ++++++++++++++++++
 src/stage0/init/lean/compiler/ir/borrow.cpp  |   39 +-
 src/stage0/init/lean/compiler/ir/emitcpp.cpp |  930 +++++++------
 13 files changed, 1838 insertions(+), 650 deletions(-)
 delete mode 100644 library/init/lean/compiler/export.lean
 create mode 100644 library/init/lean/compiler/exportattr.lean
 delete mode 100644 src/stage0/init/lean/compiler/export.cpp
 create mode 100644 src/stage0/init/lean/compiler/exportattr.cpp

diff --git a/library/init/lean/compiler/export.lean b/library/init/lean/compiler/export.lean
deleted file mode 100644
index b7d4a66d77..0000000000
--- a/library/init/lean/compiler/export.lean
+++ /dev/null
@@ -1,15 +0,0 @@
-/-
-Copyright (c) 2019 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import init.lean.environment
-
-namespace Lean
-@[extern "lean_get_export_name_for"]
-constant getExportNameFor (env : @& Environment) (n : @& Name) : Option Name := default _
-
-def isExport (env : Environment) (n : Name) : Bool :=
-(getExportNameFor env n).isSome
-end Lean
diff --git a/library/init/lean/compiler/exportattr.lean b/library/init/lean/compiler/exportattr.lean
new file mode 100644
index 0000000000..9e32804896
--- /dev/null
+++ b/library/init/lean/compiler/exportattr.lean
@@ -0,0 +1,38 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import init.lean.attributes
+
+namespace Lean
+
+private def isValidCppId (id : String) : Bool :=
+let first := id.get 0 in
+first.isAlpha  && (id.toSubstring.drop 1).all (λ c, c.isAlpha || c.isDigit || c == '_')
+
+private def isValidCppName : Name → Bool
+| (Name.mkString Name.anonymous s) := isValidCppId s
+| (Name.mkString p s) := isValidCppId s && isValidCppName p
+| _ := false
+
+def mkExportAttr : IO (ParametricAttribute Name) :=
+registerParametricAttribute `export "name to be used by code generators" $ λ env declName stx,
+  match stx with
+  | Syntax.ident _ _ exportName _ _ :=
+    if isValidCppName exportName then Except.ok exportName
+    else Except.error "invalid 'export' function name, is not a valid C++ identifier"
+  | _ := Except.error "unexpected kind of argument"
+
+@[init mkExportAttr]
+constant exportAttr : ParametricAttribute Name := default _
+
+@[export lean.get_export_name_for_core]
+def getExportNameFor (env : Environment) (n : Name) : Option Name :=
+exportAttr.getParam env n
+
+def isExport (env : Environment) (n : Name) : Bool :=
+(getExportNameFor env n).isSome
+
+end Lean
diff --git a/library/init/lean/compiler/ir/borrow.lean b/library/init/lean/compiler/ir/borrow.lean
index 62e5cb994c..b9f30de5d2 100644
--- a/library/init/lean/compiler/ir/borrow.lean
+++ b/library/init/lean/compiler/ir/borrow.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.lean.compiler.export
+import init.lean.compiler.exportattr
 import init.lean.compiler.ir.compilerm
 import init.lean.compiler.ir.normids
 
diff --git a/library/init/lean/compiler/ir/emitcpp.lean b/library/init/lean/compiler/ir/emitcpp.lean
index 5eb78917c1..546c3cbdca 100644
--- a/library/init/lean/compiler/ir/emitcpp.lean
+++ b/library/init/lean/compiler/ir/emitcpp.lean
@@ -7,7 +7,7 @@ prelude
 import init.control.conditional
 import init.lean.runtime
 import init.lean.name_mangling
-import init.lean.compiler.export
+import init.lean.compiler.exportattr
 import init.lean.compiler.initattr
 import init.lean.compiler.ir.compilerm
 import init.lean.compiler.ir.emitutil
diff --git a/src/library/compiler/export_attribute.cpp b/src/library/compiler/export_attribute.cpp
index 1c218f36a0..29d52946db 100644
--- a/src/library/compiler/export_attribute.cpp
+++ b/src/library/compiler/export_attribute.cpp
@@ -9,59 +9,8 @@ Author: Leonardo de Moura
 #include "library/util.h"
 
 namespace lean {
-struct export_attr_data : public attr_data {
-    name m_id;
-    export_attr_data(name const & id): m_id(id) {}
-    export_attr_data() {}
-
-    virtual unsigned hash() const override { return m_id.hash(); }
-    virtual void parse(expr const & e) override {
-        buffer<expr> args; get_app_args(e, args);
-        if (args.size() != 1 || !is_const(extract_mdata(args[0])))
-            throw parser_error("constant expected", get_pos_info_provider()->get_pos_info_or_some(e));
-        m_id = const_name(extract_mdata(args[0]));
-    }
-    virtual void print(std::ostream & out) override { out << " " << m_id; }
-    void write(serializer & s) const { s << m_id; }
-    void read(deserializer & d) { m_id = read_name(d); }
-};
-
-typedef typed_attribute<export_attr_data> export_attr;
-
-static export_attr const & get_export_attr() {
-    return static_cast<export_attr const &>(get_system_attribute("export"));
-}
-
+object* get_export_name_for_core(object* env, object *n);
 optional<name> get_export_name_for(environment const & env, name const & n) {
-    if (auto const & data = get_export_attr().get(env, n)) {
-        return optional<name>(data->m_id);
-    } else {
-        return optional<name>();
-    }
-}
-
-extern "C" obj_res lean_get_export_name_for(b_obj_arg env, b_obj_arg n) {
-    return to_object(get_export_name_for(environment(env, true), name(n, true)));
-}
-
-void initialize_export_attribute() {
-    register_system_attribute(export_attr("export", "name to be used by code generators",
-                                          [](environment const & env, io_state const &, name const & n, unsigned, bool persistent) {
-                                              if (!persistent) throw exception("invalid [export] attribute, must be persistent");
-                                              auto const & data = *get_export_attr().get(env, n);
-                                              name it = data.m_id;
-                                              if (it.is_anonymous()) throw exception("invalid [export] attribute, argument is missing");
-                                              while (!it.is_anonymous()) {
-                                                  if (!it.is_string()) throw exception("invalid [export] attribute, identifier cannot be numeric");
-                                                  it = it.get_prefix();
-                                              }
-                                              constant_info cinfo = env.get(n);
-                                              if (!cinfo.is_definition())
-                                                  throw exception("invalid '[export]' use, only definitions can be exported");
-                                              return env;
-                                          }));
-}
-
-void finalize_export_attribute() {
+    return to_optional<name>(get_export_name_for_core(env.to_obj_arg(), n.to_obj_arg()));
 }
 }
diff --git a/src/library/compiler/export_attribute.h b/src/library/compiler/export_attribute.h
index 10d8aa5af2..81744fdd80 100644
--- a/src/library/compiler/export_attribute.h
+++ b/src/library/compiler/export_attribute.h
@@ -9,6 +9,4 @@ Author: Leonardo de Moura
 namespace lean {
 optional<name> get_export_name_for(environment const & env, name const & n);
 inline bool has_export_name(environment const & env, name const & n) { return static_cast<bool>(get_export_name_for(env, n)); }
-void initialize_export_attribute();
-void finalize_export_attribute();
 }
diff --git a/src/library/compiler/init_module.cpp b/src/library/compiler/init_module.cpp
index 2b23756eeb..aa89476ccd 100644
--- a/src/library/compiler/init_module.cpp
+++ b/src/library/compiler/init_module.cpp
@@ -11,7 +11,6 @@ Author: Leonardo de Moura
 #include "library/compiler/specialize.h"
 #include "library/compiler/llnf.h"
 #include "library/compiler/compiler.h"
-#include "library/compiler/export_attribute.h"
 #include "library/compiler/extern_attribute.h"
 #include "library/compiler/implemented_by_attribute.h"
 #include "library/compiler/borrowed_annotation.h"
@@ -27,7 +26,6 @@ void initialize_compiler_module() {
     initialize_specialize();
     initialize_llnf();
     initialize_compiler();
-    initialize_export_attribute();
     initialize_extern_attribute();
     initialize_borrowed_annotation();
     initialize_ll_infer_type();
@@ -37,7 +35,6 @@ void finalize_compiler_module() {
     finalize_ll_infer_type();
     finalize_borrowed_annotation();
     finalize_extern_attribute();
-    finalize_export_attribute();
     finalize_compiler();
     finalize_llnf();
     finalize_specialize();
diff --git a/src/stage0/CMakeLists.txt b/src/stage0/CMakeLists.txt
index 5207036620..7fcbf8ca1a 100644
--- a/src/stage0/CMakeLists.txt
+++ b/src/stage0/CMakeLists.txt
@@ -1 +1 @@
-add_library (stage0 OBJECT ./init/coe.cpp ./init/control/alternative.cpp ./init/control/applicative.cpp ./init/control/combinators.cpp ./init/control/conditional.cpp ./init/control/default.cpp ./init/control/estate.cpp ./init/control/except.cpp ./init/control/functor.cpp ./init/control/id.cpp ./init/control/lift.cpp ./init/control/monad.cpp ./init/control/monadfail.cpp ./init/control/option.cpp ./init/control/reader.cpp ./init/control/state.cpp ./init/core.cpp ./init/data/array/basic.cpp ./init/data/array/binsearch.cpp ./init/data/array/default.cpp ./init/data/array/qsort.cpp ./init/data/assoclist.cpp ./init/data/basic.cpp ./init/data/bytearray/basic.cpp ./init/data/bytearray/default.cpp ./init/data/char/basic.cpp ./init/data/char/default.cpp ./init/data/default.cpp ./init/data/dlist.cpp ./init/data/fin/basic.cpp ./init/data/fin/default.cpp ./init/data/hashable.cpp ./init/data/hashmap/basic.cpp ./init/data/hashmap/default.cpp ./init/data/int/basic.cpp ./init/data/int/default.cpp ./init/data/list/basic.cpp ./init/data/list/default.cpp ./init/data/list/instances.cpp ./init/data/nat/basic.cpp ./init/data/nat/bitwise.cpp ./init/data/nat/default.cpp ./init/data/nat/div.cpp ./init/data/option/basic.cpp ./init/data/option/instances.cpp ./init/data/ordering/basic.cpp ./init/data/ordering/default.cpp ./init/data/persistentarray/basic.cpp ./init/data/persistentarray/default.cpp ./init/data/random.cpp ./init/data/rbmap/basic.cpp ./init/data/rbmap/default.cpp ./init/data/rbtree/basic.cpp ./init/data/rbtree/default.cpp ./init/data/repr.cpp ./init/data/string/basic.cpp ./init/data/string/default.cpp ./init/data/tostring.cpp ./init/data/uint.cpp ./init/default.cpp ./init/env_ext.cpp ./init/fix.cpp ./init/io.cpp ./init/lean/attributes.cpp ./init/lean/compiler/closedtermcache.cpp ./init/lean/compiler/constfolding.cpp ./init/lean/compiler/default.cpp ./init/lean/compiler/export.cpp ./init/lean/compiler/initattr.cpp ./init/lean/compiler/inline.cpp ./init/lean/compiler/ir/basic.cpp ./init/lean/compiler/ir/borrow.cpp ./init/lean/compiler/ir/boxing.cpp ./init/lean/compiler/ir/checker.cpp ./init/lean/compiler/ir/compilerm.cpp ./init/lean/compiler/ir/default.cpp ./init/lean/compiler/ir/elimdead.cpp ./init/lean/compiler/ir/emitcpp.cpp ./init/lean/compiler/ir/emitutil.cpp ./init/lean/compiler/ir/expandresetreuse.cpp ./init/lean/compiler/ir/format.cpp ./init/lean/compiler/ir/freevars.cpp ./init/lean/compiler/ir/livevars.cpp ./init/lean/compiler/ir/normids.cpp ./init/lean/compiler/ir/pushproj.cpp ./init/lean/compiler/ir/rc.cpp ./init/lean/compiler/ir/resetreuse.cpp ./init/lean/compiler/ir/simpcase.cpp ./init/lean/compiler/util.cpp ./init/lean/declaration.cpp ./init/lean/default.cpp ./init/lean/disjoint_set.cpp ./init/lean/environment.cpp ./init/lean/evalconst.cpp ./init/lean/expr.cpp ./init/lean/extern.cpp ./init/lean/format.cpp ./init/lean/kvmap.cpp ./init/lean/level.cpp ./init/lean/message.cpp ./init/lean/modifiers.cpp ./init/lean/name.cpp ./init/lean/name_mangling.cpp ./init/lean/options.cpp ./init/lean/parser/default.cpp ./init/lean/parser/identifier.cpp ./init/lean/parser/level.cpp ./init/lean/parser/parser.cpp ./init/lean/parser/trie.cpp ./init/lean/position.cpp ./init/lean/runtime.cpp ./init/lean/smap.cpp ./init/lean/syntax.cpp ./init/lean/toexpr.cpp ./init/lean/trace.cpp ./init/lean/util.cpp ./init/platform.cpp ./init/util.cpp ./init/wf.cpp)
+add_library (stage0 OBJECT ./init/coe.cpp ./init/control/alternative.cpp ./init/control/applicative.cpp ./init/control/combinators.cpp ./init/control/conditional.cpp ./init/control/default.cpp ./init/control/estate.cpp ./init/control/except.cpp ./init/control/functor.cpp ./init/control/id.cpp ./init/control/lift.cpp ./init/control/monad.cpp ./init/control/monadfail.cpp ./init/control/option.cpp ./init/control/reader.cpp ./init/control/state.cpp ./init/core.cpp ./init/data/array/basic.cpp ./init/data/array/binsearch.cpp ./init/data/array/default.cpp ./init/data/array/qsort.cpp ./init/data/assoclist.cpp ./init/data/basic.cpp ./init/data/bytearray/basic.cpp ./init/data/bytearray/default.cpp ./init/data/char/basic.cpp ./init/data/char/default.cpp ./init/data/default.cpp ./init/data/dlist.cpp ./init/data/fin/basic.cpp ./init/data/fin/default.cpp ./init/data/hashable.cpp ./init/data/hashmap/basic.cpp ./init/data/hashmap/default.cpp ./init/data/int/basic.cpp ./init/data/int/default.cpp ./init/data/list/basic.cpp ./init/data/list/default.cpp ./init/data/list/instances.cpp ./init/data/nat/basic.cpp ./init/data/nat/bitwise.cpp ./init/data/nat/default.cpp ./init/data/nat/div.cpp ./init/data/option/basic.cpp ./init/data/option/instances.cpp ./init/data/ordering/basic.cpp ./init/data/ordering/default.cpp ./init/data/persistentarray/basic.cpp ./init/data/persistentarray/default.cpp ./init/data/random.cpp ./init/data/rbmap/basic.cpp ./init/data/rbmap/default.cpp ./init/data/rbtree/basic.cpp ./init/data/rbtree/default.cpp ./init/data/repr.cpp ./init/data/string/basic.cpp ./init/data/string/default.cpp ./init/data/tostring.cpp ./init/data/uint.cpp ./init/default.cpp ./init/env_ext.cpp ./init/fix.cpp ./init/io.cpp ./init/lean/attributes.cpp ./init/lean/compiler/closedtermcache.cpp ./init/lean/compiler/constfolding.cpp ./init/lean/compiler/default.cpp ./init/lean/compiler/exportattr.cpp ./init/lean/compiler/initattr.cpp ./init/lean/compiler/inline.cpp ./init/lean/compiler/ir/basic.cpp ./init/lean/compiler/ir/borrow.cpp ./init/lean/compiler/ir/boxing.cpp ./init/lean/compiler/ir/checker.cpp ./init/lean/compiler/ir/compilerm.cpp ./init/lean/compiler/ir/default.cpp ./init/lean/compiler/ir/elimdead.cpp ./init/lean/compiler/ir/emitcpp.cpp ./init/lean/compiler/ir/emitutil.cpp ./init/lean/compiler/ir/expandresetreuse.cpp ./init/lean/compiler/ir/format.cpp ./init/lean/compiler/ir/freevars.cpp ./init/lean/compiler/ir/livevars.cpp ./init/lean/compiler/ir/normids.cpp ./init/lean/compiler/ir/pushproj.cpp ./init/lean/compiler/ir/rc.cpp ./init/lean/compiler/ir/resetreuse.cpp ./init/lean/compiler/ir/simpcase.cpp ./init/lean/compiler/util.cpp ./init/lean/declaration.cpp ./init/lean/default.cpp ./init/lean/disjoint_set.cpp ./init/lean/environment.cpp ./init/lean/evalconst.cpp ./init/lean/expr.cpp ./init/lean/extern.cpp ./init/lean/format.cpp ./init/lean/kvmap.cpp ./init/lean/level.cpp ./init/lean/message.cpp ./init/lean/modifiers.cpp ./init/lean/name.cpp ./init/lean/name_mangling.cpp ./init/lean/options.cpp ./init/lean/parser/default.cpp ./init/lean/parser/identifier.cpp ./init/lean/parser/level.cpp ./init/lean/parser/parser.cpp ./init/lean/parser/trie.cpp ./init/lean/position.cpp ./init/lean/runtime.cpp ./init/lean/smap.cpp ./init/lean/syntax.cpp ./init/lean/toexpr.cpp ./init/lean/trace.cpp ./init/lean/util.cpp ./init/platform.cpp ./init/util.cpp ./init/wf.cpp)
diff --git a/src/stage0/init/core.cpp b/src/stage0/init/core.cpp
index 5557e0f8ed..9b82bedb1c 100644
--- a/src/stage0/init/core.cpp
+++ b/src/stage0/init/core.cpp
@@ -67,7 +67,6 @@ obj* l_Fun_Inhabited___rarg(obj*, obj*);
 obj* l_Quotient_mk___boxed(obj*, obj*);
 obj* l_Sum_sizeof(obj*, obj*);
 obj* l_Thunk_pure(obj*, obj*);
-obj* l___private_init_core_22__extfunApp___rarg(obj*, obj*);
 obj* l_decidableOfDecidableOfIff(obj*, obj*);
 obj* l_defaultHasSizeof(obj*);
 obj* l_arbitrary___rarg___boxed(obj*);
@@ -94,7 +93,6 @@ obj* l_decidableOfDecidableOfIff___rarg___boxed(obj*, obj*);
 uint8 l_and(uint8, uint8);
 obj* l_ite___rarg___boxed(obj*, obj*, obj*, obj*);
 obj* l_or___main___boxed(obj*, obj*);
-obj* l___private_init_core_22__extfunApp(obj*, obj*);
 obj* l_Option_HasSizeof___rarg(obj*);
 obj* l_Subtype_sizeof___main___rarg(obj*, obj*, obj*);
 obj* l_bne(obj*);
@@ -124,9 +122,9 @@ obj* l_Sigma_sizeof___at_Sigma_HasSizeof___spec__1(obj*, obj*);
 obj* l_Quotient_recOnSubsingleton_u2082___at_Quotient_DecidableEq___spec__1___boxed(obj*, obj*);
 obj* l_default_sizeof___main(obj*, obj*);
 obj* l_Sigma_HasSizeof___boxed(obj*, obj*);
-obj* l___private_init_core_22__extfunApp___boxed(obj*, obj*);
 obj* l_std_priority_default;
 obj* l_Quotient_DecidableEq___rarg(obj*, obj*, obj*, obj*);
+obj* l___private_init_core_20__funSetoid(obj*, obj*);
 obj* l_arbitrary___rarg(obj*);
 obj* l_Prod_HasSizeof(obj*, obj*);
 obj* l_Subtype_sizeof___main(obj*);
@@ -146,6 +144,7 @@ obj* l_dite(obj*);
 obj* l_Thunk_mk(obj*, obj*);
 obj* l_Eq_ndrecOn___rarg___boxed(obj*);
 obj* l_Task_bind(obj*, obj*, obj*, obj*);
+obj* l___private_init_core_21__extfunApp___rarg(obj*, obj*);
 obj* l_Thunk_map(obj*, obj*, obj*, obj*);
 obj* l_dite___rarg___boxed(obj*, obj*, obj*, obj*);
 obj* l_Quotient_lift_u2082___boxed(obj*, obj*, obj*, obj*, obj*);
@@ -186,6 +185,7 @@ obj* l_Nat_sizeof(obj*);
 obj* l_Quot_indep___boxed(obj*, obj*, obj*);
 obj* l_List_HasSizeof(obj*);
 obj* l_Prod_sizeof___main___rarg(obj*, obj*, obj*);
+obj* l___private_init_core_20__funSetoid___boxed(obj*, obj*);
 obj* l_Quotient_hrecOn(obj*, obj*, obj*);
 obj* l_Option_sizeof___main___rarg(obj*, obj*);
 obj* l_Quotient_liftOn_u2082(obj*, obj*, obj*, obj*, obj*);
@@ -238,7 +238,6 @@ obj* l_std_prec_maxPlus;
 obj* l_Or_Decidable(obj*, obj*);
 obj* l_Prod_map___main___rarg(obj*, obj*, obj*);
 uint8 l_ite_Decidable___rarg(uint8, uint8, uint8);
-obj* l___private_init_core_21__funSetoid(obj*, obj*);
 obj* l_Quot_hrecOn___boxed(obj*, obj*, obj*);
 uint8 l_Decidable_decide___rarg(uint8);
 obj* l_Xor_Decidable(obj*, obj*);
@@ -340,6 +339,7 @@ obj* l_idRhs(obj*);
 obj* l_Quot_hrecOn(obj*, obj*, obj*);
 obj* l_and___main___boxed(obj*, obj*);
 obj* l_List_sizeof___main___rarg(obj*, obj*);
+obj* l___private_init_core_21__extfunApp___boxed(obj*, obj*);
 obj* l_Quotient_mk___rarg___boxed(obj*);
 obj* l_Quot_rec___rarg(obj*, obj*, obj*);
 obj* l_PointedType_Inhabited;
@@ -353,6 +353,7 @@ obj* l_Function_combine(obj*, obj*, obj*, obj*, obj*);
 obj* l_Nat_sizeof___boxed(obj*);
 obj* l_Quotient_recOnSubsingleton_u2082___boxed(obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l_Decidable_recOnTrue(obj*);
+obj* l___private_init_core_21__extfunApp(obj*, obj*);
 obj* l_PSigma_sizeof___main___at_PSigma_HasSizeof___spec__2___rarg(obj*, obj*, obj*);
 obj* l_Nat_HasAdd;
 obj* l_Subtype_Inhabited___rarg(obj*, obj*);
@@ -402,7 +403,6 @@ obj* l_implies_Decidable(obj*, obj*);
 obj* l_setoidHasEquiv___boxed(obj*, obj*);
 obj* l_Sigma_sizeof___at_Sigma_HasSizeof___spec__1___boxed(obj*, obj*);
 uint8 l_or___main(uint8, uint8);
-obj* l___private_init_core_21__funSetoid___boxed(obj*, obj*);
 uint8 l_strictAnd(uint8, uint8);
 obj* l_Eq_mp___rarg(obj*);
 obj* l_Quotient_hrecOn___boxed(obj*, obj*, obj*);
@@ -4212,7 +4212,7 @@ lean::dec(x_1);
 return x_5;
 }
 }
-obj* l___private_init_core_21__funSetoid(obj* x_1, obj* x_2) {
+obj* l___private_init_core_20__funSetoid(obj* x_1, obj* x_2) {
 _start:
 {
 obj* x_3; 
@@ -4220,16 +4220,16 @@ x_3 = lean::box(0);
 return x_3;
 }
 }
-obj* l___private_init_core_21__funSetoid___boxed(obj* x_1, obj* x_2) {
+obj* l___private_init_core_20__funSetoid___boxed(obj* x_1, obj* x_2) {
 _start:
 {
 obj* x_3; 
-x_3 = l___private_init_core_21__funSetoid(x_1, x_2);
+x_3 = l___private_init_core_20__funSetoid(x_1, x_2);
 lean::dec(x_2);
 return x_3;
 }
 }
-obj* l___private_init_core_22__extfunApp___rarg(obj* x_1, obj* x_2) {
+obj* l___private_init_core_21__extfunApp___rarg(obj* x_1, obj* x_2) {
 _start:
 {
 obj* x_3; 
@@ -4237,19 +4237,19 @@ x_3 = lean::apply_1(x_1, x_2);
 return x_3;
 }
 }
-obj* l___private_init_core_22__extfunApp(obj* x_1, obj* x_2) {
+obj* l___private_init_core_21__extfunApp(obj* x_1, obj* x_2) {
 _start:
 {
 obj* x_3; 
-x_3 = lean::alloc_closure(reinterpret_cast<void*>(l___private_init_core_22__extfunApp___rarg), 2, 0);
+x_3 = lean::alloc_closure(reinterpret_cast<void*>(l___private_init_core_21__extfunApp___rarg), 2, 0);
 return x_3;
 }
 }
-obj* l___private_init_core_22__extfunApp___boxed(obj* x_1, obj* x_2) {
+obj* l___private_init_core_21__extfunApp___boxed(obj* x_1, obj* x_2) {
 _start:
 {
 obj* x_3; 
-x_3 = l___private_init_core_22__extfunApp(x_1, x_2);
+x_3 = l___private_init_core_21__extfunApp(x_1, x_2);
 lean::dec(x_2);
 return x_3;
 }
diff --git a/src/stage0/init/lean/compiler/export.cpp b/src/stage0/init/lean/compiler/export.cpp
deleted file mode 100644
index ccb1129c06..0000000000
--- a/src/stage0/init/lean/compiler/export.cpp
+++ /dev/null
@@ -1,71 +0,0 @@
-// Lean compiler output
-// Module: init.lean.compiler.export
-// Imports: init.lean.environment
-#include "runtime/object.h"
-#include "runtime/apply.h"
-typedef lean::object obj;    typedef lean::usize  usize;
-typedef lean::uint8  uint8;  typedef lean::uint16 uint16;
-typedef lean::uint32 uint32; typedef lean::uint64 uint64;
-#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
-obj* l_Lean_getExportNameFor___boxed(obj*, obj*);
-extern "C" obj* lean_get_export_name_for(obj*, obj*);
-uint8 l_Lean_isExport(obj*, obj*);
-obj* l_Lean_isExport___boxed(obj*, obj*);
-obj* l_Lean_getExportNameFor___boxed(obj* x_1, obj* x_2) {
-_start:
-{
-obj* x_3; 
-x_3 = lean_get_export_name_for(x_1, x_2);
-return x_3;
-}
-}
-uint8 l_Lean_isExport(obj* x_1, obj* x_2) {
-_start:
-{
-obj* x_3; 
-x_3 = lean_get_export_name_for(x_1, x_2);
-if (lean::obj_tag(x_3) == 0)
-{
-uint8 x_4; 
-x_4 = 0;
-return x_4;
-}
-else
-{
-uint8 x_5; 
-lean::dec(x_3);
-x_5 = 1;
-return x_5;
-}
-}
-}
-obj* l_Lean_isExport___boxed(obj* x_1, obj* x_2) {
-_start:
-{
-uint8 x_3; obj* x_4; 
-x_3 = l_Lean_isExport(x_1, x_2);
-lean::dec(x_2);
-lean::dec(x_1);
-x_4 = lean::box(x_3);
-return x_4;
-}
-}
-obj* initialize_init_lean_environment(obj*);
-static bool _G_initialized = false;
-obj* initialize_init_lean_compiler_export(obj* w) {
-if (_G_initialized) return w;
-_G_initialized = true;
-if (io_result_is_error(w)) return w;
-w = initialize_init_lean_environment(w);
-if (io_result_is_error(w)) return w;
-REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name("Lean"), "getExportNameFor"), 2, l_Lean_getExportNameFor___boxed);
-REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name("Lean"), "isExport"), 2, l_Lean_isExport___boxed);
-return w;
-}
diff --git a/src/stage0/init/lean/compiler/exportattr.cpp b/src/stage0/init/lean/compiler/exportattr.cpp
new file mode 100644
index 0000000000..b8c9174c2a
--- /dev/null
+++ b/src/stage0/init/lean/compiler/exportattr.cpp
@@ -0,0 +1,1303 @@
+// Lean compiler output
+// Module: init.lean.compiler.exportattr
+// Imports: init.lean.attributes
+#include "runtime/object.h"
+#include "runtime/apply.h"
+typedef lean::object obj;    typedef lean::usize  usize;
+typedef lean::uint8  uint8;  typedef lean::uint16 uint16;
+typedef lean::uint32 uint32; typedef lean::uint64 uint64;
+#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
+extern "C" uint8 lean_name_dec_eq(obj*, obj*);
+obj* l_Lean_AttributeImpl_inhabited___lambda__4___boxed(obj*, obj*, obj*);
+extern obj* l_Array_empty___closed__1;
+namespace lean {
+obj* nat_sub(obj*, obj*);
+}
+obj* l_Lean_mkExportAttr___closed__2;
+obj* l_Lean_registerParametricAttribute___at_Lean_mkExportAttr___spec__1(obj*, obj*, obj*, obj*);
+obj* l_Lean_AttributeImpl_inhabited___lambda__3___boxed(obj*, obj*, obj*, obj*);
+namespace lean {
+obj* get_export_name_for_core(obj*, obj*);
+}
+obj* l_Lean_mkExportAttr___lambda__1(obj*, obj*, obj*);
+obj* l_Lean_PersistentEnvExtension_inhabited___rarg___lambda__1___boxed(obj*);
+uint8 l_Lean_isExport(obj*, obj*);
+obj* l_String_anyAux___main___at___private_init_lean_compiler_exportattr_1__isValidCppId___spec__1___boxed(obj*, obj*, obj*);
+obj* l_RBNode_find___main___at_Lean_getExportNameFor___spec__2(obj*, obj*);
+obj* l___private_init_lean_compiler_exportattr_2__isValidCppName___main___boxed(obj*);
+obj* l_Lean_registerAttribute(obj*, obj*);
+uint8 l_Char_isAlpha(uint32);
+extern obj* l_Lean_Inhabited;
+obj* l_Lean_mkExportAttr___lambda__1___boxed(obj*, obj*, obj*);
+extern obj* l_Lean_registerParametricAttribute___rarg___closed__1;
+obj* l_Array_mkEmpty(obj*, obj*);
+obj* l_Lean_mkExportAttr(obj*);
+obj* l_Array_swap(obj*, obj*, obj*, obj*);
+obj* l___private_init_lean_compiler_exportattr_2__isValidCppName___boxed(obj*);
+uint8 l___private_init_lean_compiler_exportattr_2__isValidCppName(obj*);
+obj* l_Lean_mkExportAttr___closed__1;
+obj* l_Lean_AttributeImpl_inhabited___lambda__5(obj*, obj*);
+obj* l_Lean_PersistentEnvExtension_getState___rarg(obj*, obj*);
+obj* l_Lean_registerParametricAttribute___at_Lean_mkExportAttr___spec__1___lambda__1___boxed(obj*);
+obj* l_Lean_Environment_getModuleIdxFor(obj*, obj*);
+obj* l_RBNode_find___main___at_Lean_getExportNameFor___spec__2___boxed(obj*, obj*);
+obj* l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_mkExportAttr___spec__4(obj*, obj*, obj*, obj*, obj*);
+extern obj* l_Lean_registerParametricAttribute___rarg___closed__2;
+namespace lean {
+uint8 nat_dec_lt(obj*, obj*);
+}
+obj* l_Lean_registerParametricAttribute___at_Lean_mkExportAttr___spec__1___lambda__1(obj*);
+extern obj* l_Lean_registerTagAttribute___closed__6;
+obj* l_Lean_AttributeImpl_inhabited___lambda__1___boxed(obj*, obj*, obj*, obj*, obj*);
+extern "C" obj* lean_name_mk_string(obj*, obj*);
+namespace lean {
+obj* nat_add(obj*, obj*);
+}
+obj* l_Lean_PersistentEnvExtension_getModuleEntries___rarg(obj*, obj*, obj*);
+namespace lean {
+uint8 nat_dec_eq(obj*, obj*);
+}
+obj* l_RBNode_fold___main___at_Lean_mkExportAttr___spec__2(obj*, obj*);
+obj* l_ExceptT_Monad___rarg___lambda__8___boxed(obj*, obj*);
+uint8 l___private_init_lean_compiler_exportattr_2__isValidCppName___main(obj*);
+obj* l_Array_push(obj*, obj*, obj*);
+obj* l_Lean_ParametricAttribute_getParam___at_Lean_getExportNameFor___spec__1___boxed(obj*, obj*, obj*);
+namespace lean {
+uint32 string_utf8_get(obj*, obj*);
+}
+uint8 l_UInt32_decEq(uint32, uint32);
+obj* l___private_init_lean_compiler_exportattr_1__isValidCppId___boxed(obj*);
+obj* l_Lean_registerParametricAttribute___rarg___lambda__4___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*);
+uint8 l_Char_isDigit(uint32);
+obj* l_Lean_registerParametricAttribute___at_Lean_mkExportAttr___spec__1___closed__1;
+obj* l_Lean_mkExportAttr___lambda__1___closed__1;
+obj* l_Lean_registerTagAttribute___lambda__7___boxed(obj*, obj*, obj*, obj*, obj*);
+obj* l_Lean_exportAttr;
+uint8 l_Lean_Name_quickLt(obj*, obj*);
+obj* l_Array_binSearchAux___main___at_Lean_getExportNameFor___spec__3___boxed(obj*, obj*, obj*, obj*);
+obj* l_Lean_PersistentEnvExtension_inhabited___rarg___lambda__2___boxed(obj*);
+obj* l_Array_size(obj*, obj*);
+obj* l_Array_get(obj*, obj*, obj*, obj*);
+namespace lean {
+obj* string_utf8_next(obj*, obj*);
+}
+uint8 l___private_init_lean_compiler_exportattr_1__isValidCppId___closed__1;
+extern obj* l_Lean_registerTagAttribute___closed__5;
+obj* l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_mkExportAttr___spec__4___closed__1;
+namespace lean {
+uint8 nat_dec_le(obj*, obj*);
+}
+namespace lean {
+obj* string_utf8_byte_size(obj*);
+}
+uint8 l___private_init_lean_compiler_exportattr_1__isValidCppId(obj*);
+obj* l_Lean_mkExportAttr___lambda__1___closed__2;
+namespace lean {
+obj* nat_div(obj*, obj*);
+}
+obj* l_Array_qsortAux___main___at_Lean_mkExportAttr___spec__3(obj*, obj*, obj*);
+obj* l_Lean_AttributeImpl_inhabited___lambda__2___boxed(obj*, obj*, obj*, obj*);
+obj* l_RBNode_fold___main___at_Lean_mkExportAttr___spec__2___boxed(obj*, obj*);
+obj* l_Lean_mkExportAttr___closed__3;
+obj* l_Lean_registerPersistentEnvExtensionUnsafe___rarg(obj*, obj*);
+uint8 l_String_anyAux___main___at___private_init_lean_compiler_exportattr_1__isValidCppId___spec__1(obj*, obj*, obj*);
+obj* l_Lean_ParametricAttribute_getParam___at_Lean_getExportNameFor___spec__1(obj*, obj*, obj*);
+obj* l_Array_qsortAux___main___at_Lean_mkExportAttr___spec__3___boxed(obj*, obj*, obj*);
+extern obj* l_Lean_registerTagAttribute___closed__1;
+obj* l_Lean_isExport___boxed(obj*, obj*);
+obj* l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_mkExportAttr___spec__4___boxed(obj*, obj*, obj*, obj*, obj*);
+obj* l_Lean_registerTagAttribute___lambda__6___boxed(obj*, obj*, obj*, obj*, obj*);
+obj* l_Array_binSearchAux___main___at_Lean_getExportNameFor___spec__3(obj*, obj*, obj*, obj*);
+uint8 l_String_anyAux___main___at___private_init_lean_compiler_exportattr_1__isValidCppId___spec__1(obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+uint8 x_4; 
+x_4 = lean::nat_dec_eq(x_3, x_2);
+if (x_4 == 0)
+{
+uint32 x_5; uint8 x_6; 
+x_5 = lean::string_utf8_get(x_1, x_3);
+x_6 = l_Char_isAlpha(x_5);
+if (x_6 == 0)
+{
+uint8 x_7; 
+x_7 = l_Char_isDigit(x_5);
+if (x_7 == 0)
+{
+uint32 x_8; uint8 x_9; 
+x_8 = 95;
+x_9 = x_5 == x_8;
+if (x_9 == 0)
+{
+uint8 x_10; 
+lean::dec(x_3);
+x_10 = 1;
+return x_10;
+}
+else
+{
+obj* x_11; 
+x_11 = lean::string_utf8_next(x_1, x_3);
+lean::dec(x_3);
+x_3 = x_11;
+goto _start;
+}
+}
+else
+{
+obj* x_13; 
+x_13 = lean::string_utf8_next(x_1, x_3);
+lean::dec(x_3);
+x_3 = x_13;
+goto _start;
+}
+}
+else
+{
+obj* x_15; 
+x_15 = lean::string_utf8_next(x_1, x_3);
+lean::dec(x_3);
+x_3 = x_15;
+goto _start;
+}
+}
+else
+{
+uint8 x_17; 
+lean::dec(x_3);
+x_17 = 0;
+return x_17;
+}
+}
+}
+uint8 _init_l___private_init_lean_compiler_exportattr_1__isValidCppId___closed__1() {
+_start:
+{
+obj* x_1; obj* x_2; obj* x_3; uint8 x_4; 
+x_1 = lean::mk_string("");
+x_2 = lean::string_utf8_byte_size(x_1);
+x_3 = lean::mk_nat_obj(0u);
+x_4 = l_String_anyAux___main___at___private_init_lean_compiler_exportattr_1__isValidCppId___spec__1(x_1, x_2, x_3);
+lean::dec(x_2);
+lean::dec(x_1);
+if (x_4 == 0)
+{
+uint8 x_5; 
+x_5 = 1;
+return x_5;
+}
+else
+{
+uint8 x_6; 
+x_6 = 0;
+return x_6;
+}
+}
+}
+uint8 l___private_init_lean_compiler_exportattr_1__isValidCppId(obj* x_1) {
+_start:
+{
+obj* x_2; uint32 x_3; uint8 x_4; 
+x_2 = lean::mk_nat_obj(0u);
+x_3 = lean::string_utf8_get(x_1, x_2);
+x_4 = l_Char_isAlpha(x_3);
+if (x_4 == 0)
+{
+uint8 x_5; 
+x_5 = 0;
+return x_5;
+}
+else
+{
+obj* x_6; obj* x_7; uint8 x_8; 
+x_6 = lean::string_utf8_byte_size(x_1);
+x_7 = lean::mk_nat_obj(1u);
+x_8 = lean::nat_dec_le(x_6, x_7);
+if (x_8 == 0)
+{
+uint8 x_9; 
+x_9 = l_String_anyAux___main___at___private_init_lean_compiler_exportattr_1__isValidCppId___spec__1(x_1, x_6, x_7);
+lean::dec(x_6);
+if (x_9 == 0)
+{
+uint8 x_10; 
+x_10 = 1;
+return x_10;
+}
+else
+{
+uint8 x_11; 
+x_11 = 0;
+return x_11;
+}
+}
+else
+{
+uint8 x_12; 
+lean::dec(x_6);
+x_12 = l___private_init_lean_compiler_exportattr_1__isValidCppId___closed__1;
+return x_12;
+}
+}
+}
+}
+obj* l_String_anyAux___main___at___private_init_lean_compiler_exportattr_1__isValidCppId___spec__1___boxed(obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+uint8 x_4; obj* x_5; 
+x_4 = l_String_anyAux___main___at___private_init_lean_compiler_exportattr_1__isValidCppId___spec__1(x_1, x_2, x_3);
+lean::dec(x_2);
+lean::dec(x_1);
+x_5 = lean::box(x_4);
+return x_5;
+}
+}
+obj* l___private_init_lean_compiler_exportattr_1__isValidCppId___boxed(obj* x_1) {
+_start:
+{
+uint8 x_2; obj* x_3; 
+x_2 = l___private_init_lean_compiler_exportattr_1__isValidCppId(x_1);
+lean::dec(x_1);
+x_3 = lean::box(x_2);
+return x_3;
+}
+}
+uint8 l___private_init_lean_compiler_exportattr_2__isValidCppName___main(obj* x_1) {
+_start:
+{
+switch (lean::obj_tag(x_1)) {
+case 0:
+{
+uint8 x_2; 
+x_2 = 0;
+return x_2;
+}
+case 1:
+{
+obj* x_3; obj* x_4; obj* x_5; uint8 x_6; 
+x_3 = lean::cnstr_get(x_1, 0);
+x_4 = lean::cnstr_get(x_1, 1);
+x_5 = lean::box(0);
+x_6 = lean_name_dec_eq(x_3, x_5);
+if (x_6 == 0)
+{
+uint8 x_7; 
+x_7 = l___private_init_lean_compiler_exportattr_1__isValidCppId(x_4);
+if (x_7 == 0)
+{
+uint8 x_8; 
+x_8 = 0;
+return x_8;
+}
+else
+{
+x_1 = x_3;
+goto _start;
+}
+}
+else
+{
+uint8 x_10; 
+x_10 = l___private_init_lean_compiler_exportattr_1__isValidCppId(x_4);
+return x_10;
+}
+}
+default: 
+{
+uint8 x_11; 
+x_11 = 0;
+return x_11;
+}
+}
+}
+}
+obj* l___private_init_lean_compiler_exportattr_2__isValidCppName___main___boxed(obj* x_1) {
+_start:
+{
+uint8 x_2; obj* x_3; 
+x_2 = l___private_init_lean_compiler_exportattr_2__isValidCppName___main(x_1);
+lean::dec(x_1);
+x_3 = lean::box(x_2);
+return x_3;
+}
+}
+uint8 l___private_init_lean_compiler_exportattr_2__isValidCppName(obj* x_1) {
+_start:
+{
+uint8 x_2; 
+x_2 = l___private_init_lean_compiler_exportattr_2__isValidCppName___main(x_1);
+return x_2;
+}
+}
+obj* l___private_init_lean_compiler_exportattr_2__isValidCppName___boxed(obj* x_1) {
+_start:
+{
+uint8 x_2; obj* x_3; 
+x_2 = l___private_init_lean_compiler_exportattr_2__isValidCppName(x_1);
+lean::dec(x_1);
+x_3 = lean::box(x_2);
+return x_3;
+}
+}
+obj* l_RBNode_fold___main___at_Lean_mkExportAttr___spec__2(obj* x_1, obj* x_2) {
+_start:
+{
+if (lean::obj_tag(x_2) == 0)
+{
+return x_1;
+}
+else
+{
+obj* x_3; obj* x_4; obj* x_5; obj* x_6; obj* x_7; obj* x_8; obj* x_9; 
+x_3 = lean::cnstr_get(x_2, 0);
+x_4 = lean::cnstr_get(x_2, 1);
+x_5 = lean::cnstr_get(x_2, 2);
+x_6 = lean::cnstr_get(x_2, 3);
+x_7 = l_RBNode_fold___main___at_Lean_mkExportAttr___spec__2(x_1, x_3);
+lean::inc(x_5);
+lean::inc(x_4);
+x_8 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_8, 0, x_4);
+lean::cnstr_set(x_8, 1, x_5);
+x_9 = lean::array_push(x_7, x_8);
+x_1 = x_9;
+x_2 = x_6;
+goto _start;
+}
+}
+}
+obj* _init_l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_mkExportAttr___spec__4___closed__1() {
+_start:
+{
+obj* x_1; obj* x_2; 
+x_1 = l_Lean_Inhabited;
+x_2 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_2, 0, x_1);
+lean::cnstr_set(x_2, 1, x_1);
+return x_2;
+}
+}
+obj* l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_mkExportAttr___spec__4(obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
+_start:
+{
+uint8 x_6; 
+x_6 = lean::nat_dec_lt(x_5, x_1);
+if (x_6 == 0)
+{
+obj* x_7; obj* x_8; 
+lean::dec(x_5);
+x_7 = lean::array_swap(x_3, x_4, x_1);
+x_8 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_8, 0, x_4);
+lean::cnstr_set(x_8, 1, x_7);
+return x_8;
+}
+else
+{
+obj* x_9; obj* x_10; obj* x_11; obj* x_12; uint8 x_13; 
+x_9 = l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_mkExportAttr___spec__4___closed__1;
+x_10 = lean::array_get(x_9, x_3, x_5);
+x_11 = lean::cnstr_get(x_10, 0);
+lean::inc(x_11);
+lean::dec(x_10);
+x_12 = lean::cnstr_get(x_2, 0);
+x_13 = l_Lean_Name_quickLt(x_11, x_12);
+lean::dec(x_11);
+if (x_13 == 0)
+{
+obj* x_14; obj* x_15; 
+x_14 = lean::mk_nat_obj(1u);
+x_15 = lean::nat_add(x_5, x_14);
+lean::dec(x_5);
+x_5 = x_15;
+goto _start;
+}
+else
+{
+obj* x_17; obj* x_18; obj* x_19; obj* x_20; 
+x_17 = lean::array_swap(x_3, x_4, x_5);
+x_18 = lean::mk_nat_obj(1u);
+x_19 = lean::nat_add(x_4, x_18);
+lean::dec(x_4);
+x_20 = lean::nat_add(x_5, x_18);
+lean::dec(x_5);
+x_3 = x_17;
+x_4 = x_19;
+x_5 = x_20;
+goto _start;
+}
+}
+}
+}
+obj* l_Array_qsortAux___main___at_Lean_mkExportAttr___spec__3(obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+uint8 x_4; 
+x_4 = lean::nat_dec_lt(x_2, x_3);
+if (x_4 == 0)
+{
+lean::dec(x_2);
+return x_1;
+}
+else
+{
+obj* x_5; obj* x_6; obj* x_7; obj* x_8; obj* x_57; obj* x_58; obj* x_59; obj* x_60; obj* x_61; uint8 x_62; 
+x_5 = lean::nat_add(x_2, x_3);
+x_6 = lean::mk_nat_obj(2u);
+x_7 = lean::nat_div(x_5, x_6);
+lean::dec(x_5);
+x_57 = l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_mkExportAttr___spec__4___closed__1;
+x_58 = lean::array_get(x_57, x_1, x_7);
+x_59 = lean::array_get(x_57, x_1, x_2);
+x_60 = lean::cnstr_get(x_58, 0);
+lean::inc(x_60);
+lean::dec(x_58);
+x_61 = lean::cnstr_get(x_59, 0);
+lean::inc(x_61);
+lean::dec(x_59);
+x_62 = l_Lean_Name_quickLt(x_60, x_61);
+lean::dec(x_61);
+lean::dec(x_60);
+if (x_62 == 0)
+{
+x_8 = x_1;
+goto block_56;
+}
+else
+{
+obj* x_63; 
+x_63 = lean::array_swap(x_1, x_2, x_7);
+x_8 = x_63;
+goto block_56;
+}
+block_56:
+{
+obj* x_9; obj* x_10; obj* x_11; obj* x_12; obj* x_13; uint8 x_14; 
+x_9 = l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_mkExportAttr___spec__4___closed__1;
+x_10 = lean::array_get(x_9, x_8, x_3);
+x_11 = lean::array_get(x_9, x_8, x_2);
+x_12 = lean::cnstr_get(x_10, 0);
+lean::inc(x_12);
+x_13 = lean::cnstr_get(x_11, 0);
+lean::inc(x_13);
+lean::dec(x_11);
+x_14 = l_Lean_Name_quickLt(x_12, x_13);
+lean::dec(x_13);
+if (x_14 == 0)
+{
+obj* x_15; obj* x_16; uint8 x_17; 
+x_15 = lean::array_get(x_9, x_8, x_7);
+x_16 = lean::cnstr_get(x_15, 0);
+lean::inc(x_16);
+lean::dec(x_15);
+x_17 = l_Lean_Name_quickLt(x_16, x_12);
+lean::dec(x_12);
+lean::dec(x_16);
+if (x_17 == 0)
+{
+obj* x_18; obj* x_19; obj* x_20; obj* x_21; obj* x_22; obj* x_23; 
+lean::dec(x_7);
+lean::inc(x_2, 2);
+x_18 = l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_mkExportAttr___spec__4(x_3, x_10, x_8, x_2, x_2);
+lean::dec(x_10);
+x_19 = lean::cnstr_get(x_18, 0);
+lean::inc(x_19);
+x_20 = lean::cnstr_get(x_18, 1);
+lean::inc(x_20);
+lean::dec(x_18);
+x_21 = l_Array_qsortAux___main___at_Lean_mkExportAttr___spec__3(x_20, x_2, x_19);
+x_22 = lean::mk_nat_obj(1u);
+x_23 = lean::nat_add(x_19, x_22);
+lean::dec(x_19);
+x_1 = x_21;
+x_2 = x_23;
+goto _start;
+}
+else
+{
+obj* x_25; obj* x_26; obj* x_27; obj* x_28; obj* x_29; obj* x_30; obj* x_31; obj* x_32; 
+lean::dec(x_10);
+x_25 = lean::array_swap(x_8, x_7, x_3);
+lean::dec(x_7);
+x_26 = lean::array_get(x_9, x_25, x_3);
+lean::inc(x_2, 2);
+x_27 = l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_mkExportAttr___spec__4(x_3, x_26, x_25, x_2, x_2);
+lean::dec(x_26);
+x_28 = lean::cnstr_get(x_27, 0);
+lean::inc(x_28);
+x_29 = lean::cnstr_get(x_27, 1);
+lean::inc(x_29);
+lean::dec(x_27);
+x_30 = l_Array_qsortAux___main___at_Lean_mkExportAttr___spec__3(x_29, x_2, x_28);
+x_31 = lean::mk_nat_obj(1u);
+x_32 = lean::nat_add(x_28, x_31);
+lean::dec(x_28);
+x_1 = x_30;
+x_2 = x_32;
+goto _start;
+}
+}
+else
+{
+obj* x_34; obj* x_35; obj* x_36; obj* x_37; obj* x_38; uint8 x_39; 
+lean::dec(x_12);
+lean::dec(x_10);
+x_34 = lean::array_swap(x_8, x_2, x_3);
+x_35 = lean::array_get(x_9, x_34, x_7);
+x_36 = lean::array_get(x_9, x_34, x_3);
+x_37 = lean::cnstr_get(x_35, 0);
+lean::inc(x_37);
+lean::dec(x_35);
+x_38 = lean::cnstr_get(x_36, 0);
+lean::inc(x_38);
+x_39 = l_Lean_Name_quickLt(x_37, x_38);
+lean::dec(x_38);
+lean::dec(x_37);
+if (x_39 == 0)
+{
+obj* x_40; obj* x_41; obj* x_42; obj* x_43; obj* x_44; obj* x_45; 
+lean::dec(x_7);
+lean::inc(x_2, 2);
+x_40 = l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_mkExportAttr___spec__4(x_3, x_36, x_34, x_2, x_2);
+lean::dec(x_36);
+x_41 = lean::cnstr_get(x_40, 0);
+lean::inc(x_41);
+x_42 = lean::cnstr_get(x_40, 1);
+lean::inc(x_42);
+lean::dec(x_40);
+x_43 = l_Array_qsortAux___main___at_Lean_mkExportAttr___spec__3(x_42, x_2, x_41);
+x_44 = lean::mk_nat_obj(1u);
+x_45 = lean::nat_add(x_41, x_44);
+lean::dec(x_41);
+x_1 = x_43;
+x_2 = x_45;
+goto _start;
+}
+else
+{
+obj* x_47; obj* x_48; obj* x_49; obj* x_50; obj* x_51; obj* x_52; obj* x_53; obj* x_54; 
+lean::dec(x_36);
+x_47 = lean::array_swap(x_34, x_7, x_3);
+lean::dec(x_7);
+x_48 = lean::array_get(x_9, x_47, x_3);
+lean::inc(x_2, 2);
+x_49 = l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_mkExportAttr___spec__4(x_3, x_48, x_47, x_2, x_2);
+lean::dec(x_48);
+x_50 = lean::cnstr_get(x_49, 0);
+lean::inc(x_50);
+x_51 = lean::cnstr_get(x_49, 1);
+lean::inc(x_51);
+lean::dec(x_49);
+x_52 = l_Array_qsortAux___main___at_Lean_mkExportAttr___spec__3(x_51, x_2, x_50);
+x_53 = lean::mk_nat_obj(1u);
+x_54 = lean::nat_add(x_50, x_53);
+lean::dec(x_50);
+x_1 = x_52;
+x_2 = x_54;
+goto _start;
+}
+}
+}
+}
+}
+}
+obj* l_Lean_registerParametricAttribute___at_Lean_mkExportAttr___spec__1___lambda__1(obj* x_1) {
+_start:
+{
+obj* x_2; obj* x_3; obj* x_4; obj* x_5; obj* x_6; obj* x_7; obj* x_8; 
+x_2 = l_Array_empty___closed__1;
+x_3 = l_RBNode_fold___main___at_Lean_mkExportAttr___spec__2(x_2, x_1);
+x_4 = lean::array_get_size(x_3);
+x_5 = lean::mk_nat_obj(1u);
+x_6 = lean::nat_sub(x_4, x_5);
+lean::dec(x_4);
+x_7 = lean::mk_nat_obj(0u);
+x_8 = l_Array_qsortAux___main___at_Lean_mkExportAttr___spec__3(x_3, x_7, x_6);
+lean::dec(x_6);
+return x_8;
+}
+}
+obj* _init_l_Lean_registerParametricAttribute___at_Lean_mkExportAttr___spec__1___closed__1() {
+_start:
+{
+obj* x_1; 
+x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_registerParametricAttribute___at_Lean_mkExportAttr___spec__1___lambda__1___boxed), 1, 0);
+return x_1;
+}
+}
+obj* l_Lean_registerParametricAttribute___at_Lean_mkExportAttr___spec__1(obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
+_start:
+{
+obj* x_5; obj* x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_10; 
+x_5 = l_Lean_registerTagAttribute___closed__1;
+x_6 = l_Lean_registerParametricAttribute___rarg___closed__1;
+x_7 = l_Lean_registerParametricAttribute___at_Lean_mkExportAttr___spec__1___closed__1;
+x_8 = l_Lean_registerParametricAttribute___rarg___closed__2;
+lean::inc(x_1);
+x_9 = lean::alloc_cnstr(0, 5, 0);
+lean::cnstr_set(x_9, 0, x_1);
+lean::cnstr_set(x_9, 1, x_5);
+lean::cnstr_set(x_9, 2, x_6);
+lean::cnstr_set(x_9, 3, x_7);
+lean::cnstr_set(x_9, 4, x_8);
+x_10 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg(x_9, x_4);
+if (lean::obj_tag(x_10) == 0)
+{
+uint8 x_11; 
+x_11 = !lean::is_exclusive(x_10);
+if (x_11 == 0)
+{
+obj* x_12; obj* x_13; obj* x_14; obj* x_15; obj* x_16; obj* x_17; obj* x_18; uint8 x_19; obj* x_20; obj* x_21; 
+x_12 = lean::cnstr_get(x_10, 0);
+x_13 = lean::box(0);
+lean::cnstr_set(x_10, 0, x_13);
+lean::inc(x_12);
+lean::inc(x_1);
+x_14 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_registerParametricAttribute___rarg___lambda__4___boxed), 8, 3);
+lean::closure_set(x_14, 0, x_1);
+lean::closure_set(x_14, 1, x_3);
+lean::closure_set(x_14, 2, x_12);
+lean::inc(x_1);
+x_15 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_registerTagAttribute___lambda__6___boxed), 5, 1);
+lean::closure_set(x_15, 0, x_1);
+lean::inc(x_1);
+x_16 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_registerTagAttribute___lambda__7___boxed), 5, 1);
+lean::closure_set(x_16, 0, x_1);
+x_17 = l_Lean_registerTagAttribute___closed__5;
+x_18 = l_Lean_registerTagAttribute___closed__6;
+x_19 = 0;
+x_20 = lean::alloc_cnstr(0, 8, 1);
+lean::cnstr_set(x_20, 0, x_1);
+lean::cnstr_set(x_20, 1, x_2);
+lean::cnstr_set(x_20, 2, x_14);
+lean::cnstr_set(x_20, 3, x_15);
+lean::cnstr_set(x_20, 4, x_16);
+lean::cnstr_set(x_20, 5, x_17);
+lean::cnstr_set(x_20, 6, x_18);
+lean::cnstr_set(x_20, 7, x_18);
+lean::cnstr_set_scalar(x_20, sizeof(void*)*8, x_19);
+lean::inc(x_20);
+x_21 = l_Lean_registerAttribute(x_20, x_10);
+if (lean::obj_tag(x_21) == 0)
+{
+uint8 x_22; 
+x_22 = !lean::is_exclusive(x_21);
+if (x_22 == 0)
+{
+obj* x_23; obj* x_24; 
+x_23 = lean::cnstr_get(x_21, 0);
+lean::dec(x_23);
+x_24 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_24, 0, x_20);
+lean::cnstr_set(x_24, 1, x_12);
+lean::cnstr_set(x_21, 0, x_24);
+return x_21;
+}
+else
+{
+obj* x_25; obj* x_26; obj* x_27; 
+x_25 = lean::cnstr_get(x_21, 1);
+lean::inc(x_25);
+lean::dec(x_21);
+x_26 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_26, 0, x_20);
+lean::cnstr_set(x_26, 1, x_12);
+x_27 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_27, 0, x_26);
+lean::cnstr_set(x_27, 1, x_25);
+return x_27;
+}
+}
+else
+{
+uint8 x_28; 
+lean::dec(x_20);
+lean::dec(x_12);
+x_28 = !lean::is_exclusive(x_21);
+if (x_28 == 0)
+{
+return x_21;
+}
+else
+{
+obj* x_29; obj* x_30; obj* x_31; 
+x_29 = lean::cnstr_get(x_21, 0);
+x_30 = lean::cnstr_get(x_21, 1);
+lean::inc(x_30);
+lean::inc(x_29);
+lean::dec(x_21);
+x_31 = lean::alloc_cnstr(1, 2, 0);
+lean::cnstr_set(x_31, 0, x_29);
+lean::cnstr_set(x_31, 1, x_30);
+return x_31;
+}
+}
+}
+else
+{
+obj* x_32; obj* x_33; obj* x_34; obj* x_35; obj* x_36; obj* x_37; obj* x_38; obj* x_39; obj* x_40; uint8 x_41; obj* x_42; obj* x_43; 
+x_32 = lean::cnstr_get(x_10, 0);
+x_33 = lean::cnstr_get(x_10, 1);
+lean::inc(x_33);
+lean::inc(x_32);
+lean::dec(x_10);
+x_34 = lean::box(0);
+x_35 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_35, 0, x_34);
+lean::cnstr_set(x_35, 1, x_33);
+lean::inc(x_32);
+lean::inc(x_1);
+x_36 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_registerParametricAttribute___rarg___lambda__4___boxed), 8, 3);
+lean::closure_set(x_36, 0, x_1);
+lean::closure_set(x_36, 1, x_3);
+lean::closure_set(x_36, 2, x_32);
+lean::inc(x_1);
+x_37 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_registerTagAttribute___lambda__6___boxed), 5, 1);
+lean::closure_set(x_37, 0, x_1);
+lean::inc(x_1);
+x_38 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_registerTagAttribute___lambda__7___boxed), 5, 1);
+lean::closure_set(x_38, 0, x_1);
+x_39 = l_Lean_registerTagAttribute___closed__5;
+x_40 = l_Lean_registerTagAttribute___closed__6;
+x_41 = 0;
+x_42 = lean::alloc_cnstr(0, 8, 1);
+lean::cnstr_set(x_42, 0, x_1);
+lean::cnstr_set(x_42, 1, x_2);
+lean::cnstr_set(x_42, 2, x_36);
+lean::cnstr_set(x_42, 3, x_37);
+lean::cnstr_set(x_42, 4, x_38);
+lean::cnstr_set(x_42, 5, x_39);
+lean::cnstr_set(x_42, 6, x_40);
+lean::cnstr_set(x_42, 7, x_40);
+lean::cnstr_set_scalar(x_42, sizeof(void*)*8, x_41);
+lean::inc(x_42);
+x_43 = l_Lean_registerAttribute(x_42, x_35);
+if (lean::obj_tag(x_43) == 0)
+{
+obj* x_44; obj* x_45; obj* x_46; obj* x_47; 
+x_44 = lean::cnstr_get(x_43, 1);
+lean::inc(x_44);
+if (lean::is_exclusive(x_43)) {
+ lean::cnstr_release(x_43, 0);
+ lean::cnstr_release(x_43, 1);
+ x_45 = x_43;
+} else {
+ lean::dec_ref(x_43);
+ x_45 = lean::box(0);
+}
+x_46 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_46, 0, x_42);
+lean::cnstr_set(x_46, 1, x_32);
+if (lean::is_scalar(x_45)) {
+ x_47 = lean::alloc_cnstr(0, 2, 0);
+} else {
+ x_47 = x_45;
+}
+lean::cnstr_set(x_47, 0, x_46);
+lean::cnstr_set(x_47, 1, x_44);
+return x_47;
+}
+else
+{
+obj* x_48; obj* x_49; obj* x_50; obj* x_51; 
+lean::dec(x_42);
+lean::dec(x_32);
+x_48 = lean::cnstr_get(x_43, 0);
+lean::inc(x_48);
+x_49 = lean::cnstr_get(x_43, 1);
+lean::inc(x_49);
+if (lean::is_exclusive(x_43)) {
+ lean::cnstr_release(x_43, 0);
+ lean::cnstr_release(x_43, 1);
+ x_50 = x_43;
+} else {
+ lean::dec_ref(x_43);
+ x_50 = lean::box(0);
+}
+if (lean::is_scalar(x_50)) {
+ x_51 = lean::alloc_cnstr(1, 2, 0);
+} else {
+ x_51 = x_50;
+}
+lean::cnstr_set(x_51, 0, x_48);
+lean::cnstr_set(x_51, 1, x_49);
+return x_51;
+}
+}
+}
+else
+{
+uint8 x_52; 
+lean::dec(x_3);
+lean::dec(x_2);
+lean::dec(x_1);
+x_52 = !lean::is_exclusive(x_10);
+if (x_52 == 0)
+{
+return x_10;
+}
+else
+{
+obj* x_53; obj* x_54; obj* x_55; 
+x_53 = lean::cnstr_get(x_10, 0);
+x_54 = lean::cnstr_get(x_10, 1);
+lean::inc(x_54);
+lean::inc(x_53);
+lean::dec(x_10);
+x_55 = lean::alloc_cnstr(1, 2, 0);
+lean::cnstr_set(x_55, 0, x_53);
+lean::cnstr_set(x_55, 1, x_54);
+return x_55;
+}
+}
+}
+}
+obj* _init_l_Lean_mkExportAttr___lambda__1___closed__1() {
+_start:
+{
+obj* x_1; obj* x_2; 
+x_1 = lean::mk_string("unexpected kind of argument");
+x_2 = lean::alloc_cnstr(0, 1, 0);
+lean::cnstr_set(x_2, 0, x_1);
+return x_2;
+}
+}
+obj* _init_l_Lean_mkExportAttr___lambda__1___closed__2() {
+_start:
+{
+obj* x_1; obj* x_2; 
+x_1 = lean::mk_string("invalid 'export' function name, is not a valid C++ identifier");
+x_2 = lean::alloc_cnstr(0, 1, 0);
+lean::cnstr_set(x_2, 0, x_1);
+return x_2;
+}
+}
+obj* l_Lean_mkExportAttr___lambda__1(obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+if (lean::obj_tag(x_3) == 3)
+{
+obj* x_4; uint8 x_5; 
+x_4 = lean::cnstr_get(x_3, 2);
+x_5 = l___private_init_lean_compiler_exportattr_2__isValidCppName___main(x_4);
+if (x_5 == 0)
+{
+obj* x_6; 
+x_6 = l_Lean_mkExportAttr___lambda__1___closed__2;
+return x_6;
+}
+else
+{
+obj* x_7; 
+lean::inc(x_4);
+x_7 = lean::alloc_cnstr(1, 1, 0);
+lean::cnstr_set(x_7, 0, x_4);
+return x_7;
+}
+}
+else
+{
+obj* x_8; 
+x_8 = l_Lean_mkExportAttr___lambda__1___closed__1;
+return x_8;
+}
+}
+}
+obj* _init_l_Lean_mkExportAttr___closed__1() {
+_start:
+{
+obj* x_1; obj* x_2; obj* x_3; 
+x_1 = lean::box(0);
+x_2 = lean::mk_string("export");
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
+obj* _init_l_Lean_mkExportAttr___closed__2() {
+_start:
+{
+obj* x_1; 
+x_1 = lean::mk_string("name to be used by code generators");
+return x_1;
+}
+}
+obj* _init_l_Lean_mkExportAttr___closed__3() {
+_start:
+{
+obj* x_1; 
+x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_mkExportAttr___lambda__1___boxed), 3, 0);
+return x_1;
+}
+}
+obj* l_Lean_mkExportAttr(obj* x_1) {
+_start:
+{
+obj* x_2; obj* x_3; obj* x_4; obj* x_5; 
+x_2 = l_Lean_mkExportAttr___closed__1;
+x_3 = l_Lean_mkExportAttr___closed__2;
+x_4 = l_Lean_mkExportAttr___closed__3;
+x_5 = l_Lean_registerParametricAttribute___at_Lean_mkExportAttr___spec__1(x_2, x_3, x_4, x_1);
+return x_5;
+}
+}
+obj* l_RBNode_fold___main___at_Lean_mkExportAttr___spec__2___boxed(obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = l_RBNode_fold___main___at_Lean_mkExportAttr___spec__2(x_1, x_2);
+lean::dec(x_2);
+return x_3;
+}
+}
+obj* l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_mkExportAttr___spec__4___boxed(obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
+_start:
+{
+obj* x_6; 
+x_6 = l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_mkExportAttr___spec__4(x_1, x_2, x_3, x_4, x_5);
+lean::dec(x_2);
+lean::dec(x_1);
+return x_6;
+}
+}
+obj* l_Array_qsortAux___main___at_Lean_mkExportAttr___spec__3___boxed(obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+obj* x_4; 
+x_4 = l_Array_qsortAux___main___at_Lean_mkExportAttr___spec__3(x_1, x_2, x_3);
+lean::dec(x_3);
+return x_4;
+}
+}
+obj* l_Lean_registerParametricAttribute___at_Lean_mkExportAttr___spec__1___lambda__1___boxed(obj* x_1) {
+_start:
+{
+obj* x_2; 
+x_2 = l_Lean_registerParametricAttribute___at_Lean_mkExportAttr___spec__1___lambda__1(x_1);
+lean::dec(x_1);
+return x_2;
+}
+}
+obj* l_Lean_mkExportAttr___lambda__1___boxed(obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+obj* x_4; 
+x_4 = l_Lean_mkExportAttr___lambda__1(x_1, x_2, x_3);
+lean::dec(x_3);
+lean::dec(x_2);
+lean::dec(x_1);
+return x_4;
+}
+}
+obj* l_RBNode_find___main___at_Lean_getExportNameFor___spec__2(obj* x_1, obj* x_2) {
+_start:
+{
+if (lean::obj_tag(x_1) == 0)
+{
+obj* x_3; 
+x_3 = lean::box(0);
+return x_3;
+}
+else
+{
+obj* x_4; obj* x_5; obj* x_6; obj* x_7; uint8 x_8; 
+x_4 = lean::cnstr_get(x_1, 0);
+x_5 = lean::cnstr_get(x_1, 1);
+x_6 = lean::cnstr_get(x_1, 2);
+x_7 = lean::cnstr_get(x_1, 3);
+x_8 = l_Lean_Name_quickLt(x_2, x_5);
+if (x_8 == 0)
+{
+uint8 x_9; 
+x_9 = l_Lean_Name_quickLt(x_5, x_2);
+if (x_9 == 0)
+{
+obj* x_10; 
+lean::inc(x_6);
+x_10 = lean::alloc_cnstr(1, 1, 0);
+lean::cnstr_set(x_10, 0, x_6);
+return x_10;
+}
+else
+{
+x_1 = x_7;
+goto _start;
+}
+}
+else
+{
+x_1 = x_4;
+goto _start;
+}
+}
+}
+}
+obj* l_Array_binSearchAux___main___at_Lean_getExportNameFor___spec__3(obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
+_start:
+{
+uint8 x_5; 
+x_5 = lean::nat_dec_le(x_3, x_4);
+if (x_5 == 0)
+{
+obj* x_6; 
+lean::dec(x_4);
+lean::dec(x_3);
+x_6 = lean::box(0);
+return x_6;
+}
+else
+{
+obj* x_7; obj* x_8; obj* x_9; obj* x_10; obj* x_11; obj* x_12; obj* x_13; uint8 x_14; 
+x_7 = lean::nat_add(x_3, x_4);
+x_8 = lean::mk_nat_obj(2u);
+x_9 = lean::nat_div(x_7, x_8);
+lean::dec(x_7);
+x_10 = l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_mkExportAttr___spec__4___closed__1;
+x_11 = lean::array_get(x_10, x_1, x_9);
+x_12 = lean::cnstr_get(x_11, 0);
+lean::inc(x_12);
+x_13 = lean::cnstr_get(x_2, 0);
+x_14 = l_Lean_Name_quickLt(x_12, x_13);
+if (x_14 == 0)
+{
+uint8 x_15; 
+lean::dec(x_4);
+x_15 = l_Lean_Name_quickLt(x_13, x_12);
+lean::dec(x_12);
+if (x_15 == 0)
+{
+obj* x_16; 
+lean::dec(x_9);
+lean::dec(x_3);
+x_16 = lean::alloc_cnstr(1, 1, 0);
+lean::cnstr_set(x_16, 0, x_11);
+return x_16;
+}
+else
+{
+obj* x_17; uint8 x_18; 
+lean::dec(x_11);
+x_17 = lean::mk_nat_obj(0u);
+x_18 = lean::nat_dec_eq(x_9, x_17);
+if (x_18 == 0)
+{
+obj* x_19; obj* x_20; 
+x_19 = lean::mk_nat_obj(1u);
+x_20 = lean::nat_sub(x_9, x_19);
+lean::dec(x_9);
+x_4 = x_20;
+goto _start;
+}
+else
+{
+obj* x_22; 
+lean::dec(x_9);
+lean::dec(x_3);
+x_22 = lean::box(0);
+return x_22;
+}
+}
+}
+else
+{
+obj* x_23; obj* x_24; 
+lean::dec(x_12);
+lean::dec(x_11);
+lean::dec(x_3);
+x_23 = lean::mk_nat_obj(1u);
+x_24 = lean::nat_add(x_9, x_23);
+lean::dec(x_9);
+x_3 = x_24;
+goto _start;
+}
+}
+}
+}
+obj* l_Lean_ParametricAttribute_getParam___at_Lean_getExportNameFor___spec__1(obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+obj* x_4; 
+x_4 = l_Lean_Environment_getModuleIdxFor(x_2, x_3);
+if (lean::obj_tag(x_4) == 0)
+{
+obj* x_5; obj* x_6; obj* x_7; 
+x_5 = lean::cnstr_get(x_1, 1);
+lean::inc(x_5);
+lean::dec(x_1);
+x_6 = l_Lean_PersistentEnvExtension_getState___rarg(x_5, x_2);
+x_7 = l_RBNode_find___main___at_Lean_getExportNameFor___spec__2(x_6, x_3);
+lean::dec(x_3);
+lean::dec(x_6);
+return x_7;
+}
+else
+{
+obj* x_8; obj* x_9; obj* x_10; obj* x_11; obj* x_12; obj* x_13; obj* x_14; obj* x_15; obj* x_16; obj* x_17; 
+x_8 = lean::cnstr_get(x_4, 0);
+lean::inc(x_8);
+lean::dec(x_4);
+x_9 = lean::cnstr_get(x_1, 1);
+lean::inc(x_9);
+lean::dec(x_1);
+x_10 = l_Lean_PersistentEnvExtension_getModuleEntries___rarg(x_9, x_2, x_8);
+lean::dec(x_8);
+x_11 = lean::box(0);
+x_12 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_12, 0, x_3);
+lean::cnstr_set(x_12, 1, x_11);
+x_13 = lean::array_get_size(x_10);
+x_14 = lean::mk_nat_obj(1u);
+x_15 = lean::nat_sub(x_13, x_14);
+lean::dec(x_13);
+x_16 = lean::mk_nat_obj(0u);
+x_17 = l_Array_binSearchAux___main___at_Lean_getExportNameFor___spec__3(x_10, x_12, x_16, x_15);
+lean::dec(x_12);
+lean::dec(x_10);
+if (lean::obj_tag(x_17) == 0)
+{
+obj* x_18; 
+x_18 = lean::box(0);
+return x_18;
+}
+else
+{
+uint8 x_19; 
+x_19 = !lean::is_exclusive(x_17);
+if (x_19 == 0)
+{
+obj* x_20; obj* x_21; 
+x_20 = lean::cnstr_get(x_17, 0);
+x_21 = lean::cnstr_get(x_20, 1);
+lean::inc(x_21);
+lean::dec(x_20);
+lean::cnstr_set(x_17, 0, x_21);
+return x_17;
+}
+else
+{
+obj* x_22; obj* x_23; obj* x_24; 
+x_22 = lean::cnstr_get(x_17, 0);
+lean::inc(x_22);
+lean::dec(x_17);
+x_23 = lean::cnstr_get(x_22, 1);
+lean::inc(x_23);
+lean::dec(x_22);
+x_24 = lean::alloc_cnstr(1, 1, 0);
+lean::cnstr_set(x_24, 0, x_23);
+return x_24;
+}
+}
+}
+}
+}
+namespace lean {
+obj* get_export_name_for_core(obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; obj* x_4; 
+x_3 = l_Lean_exportAttr;
+x_4 = l_Lean_ParametricAttribute_getParam___at_Lean_getExportNameFor___spec__1(x_3, x_1, x_2);
+lean::dec(x_1);
+return x_4;
+}
+}
+}
+obj* l_RBNode_find___main___at_Lean_getExportNameFor___spec__2___boxed(obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = l_RBNode_find___main___at_Lean_getExportNameFor___spec__2(x_1, x_2);
+lean::dec(x_2);
+lean::dec(x_1);
+return x_3;
+}
+}
+obj* l_Array_binSearchAux___main___at_Lean_getExportNameFor___spec__3___boxed(obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
+_start:
+{
+obj* x_5; 
+x_5 = l_Array_binSearchAux___main___at_Lean_getExportNameFor___spec__3(x_1, x_2, x_3, x_4);
+lean::dec(x_2);
+lean::dec(x_1);
+return x_5;
+}
+}
+obj* l_Lean_ParametricAttribute_getParam___at_Lean_getExportNameFor___spec__1___boxed(obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+obj* x_4; 
+x_4 = l_Lean_ParametricAttribute_getParam___at_Lean_getExportNameFor___spec__1(x_1, x_2, x_3);
+lean::dec(x_2);
+return x_4;
+}
+}
+uint8 l_Lean_isExport(obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; obj* x_4; 
+x_3 = l_Lean_exportAttr;
+x_4 = l_Lean_ParametricAttribute_getParam___at_Lean_getExportNameFor___spec__1(x_3, x_1, x_2);
+if (lean::obj_tag(x_4) == 0)
+{
+uint8 x_5; 
+x_5 = 0;
+return x_5;
+}
+else
+{
+uint8 x_6; 
+lean::dec(x_4);
+x_6 = 1;
+return x_6;
+}
+}
+}
+obj* l_Lean_isExport___boxed(obj* x_1, obj* x_2) {
+_start:
+{
+uint8 x_3; obj* x_4; 
+x_3 = l_Lean_isExport(x_1, x_2);
+lean::dec(x_1);
+x_4 = lean::box(x_3);
+return x_4;
+}
+}
+obj* initialize_init_lean_attributes(obj*);
+static bool _G_initialized = false;
+obj* initialize_init_lean_compiler_exportattr(obj* w) {
+if (_G_initialized) return w;
+_G_initialized = true;
+if (io_result_is_error(w)) return w;
+w = initialize_init_lean_attributes(w);
+if (io_result_is_error(w)) return w;
+l___private_init_lean_compiler_exportattr_1__isValidCppId___closed__1 = _init_l___private_init_lean_compiler_exportattr_1__isValidCppId___closed__1();
+l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_mkExportAttr___spec__4___closed__1 = _init_l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_mkExportAttr___spec__4___closed__1();
+lean::mark_persistent(l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_mkExportAttr___spec__4___closed__1);
+l_Lean_registerParametricAttribute___at_Lean_mkExportAttr___spec__1___closed__1 = _init_l_Lean_registerParametricAttribute___at_Lean_mkExportAttr___spec__1___closed__1();
+lean::mark_persistent(l_Lean_registerParametricAttribute___at_Lean_mkExportAttr___spec__1___closed__1);
+l_Lean_mkExportAttr___lambda__1___closed__1 = _init_l_Lean_mkExportAttr___lambda__1___closed__1();
+lean::mark_persistent(l_Lean_mkExportAttr___lambda__1___closed__1);
+l_Lean_mkExportAttr___lambda__1___closed__2 = _init_l_Lean_mkExportAttr___lambda__1___closed__2();
+lean::mark_persistent(l_Lean_mkExportAttr___lambda__1___closed__2);
+l_Lean_mkExportAttr___closed__1 = _init_l_Lean_mkExportAttr___closed__1();
+lean::mark_persistent(l_Lean_mkExportAttr___closed__1);
+l_Lean_mkExportAttr___closed__2 = _init_l_Lean_mkExportAttr___closed__2();
+lean::mark_persistent(l_Lean_mkExportAttr___closed__2);
+l_Lean_mkExportAttr___closed__3 = _init_l_Lean_mkExportAttr___closed__3();
+lean::mark_persistent(l_Lean_mkExportAttr___closed__3);
+REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name("Lean"), "mkExportAttr"), 1, l_Lean_mkExportAttr);
+w = l_Lean_mkExportAttr(w);
+if (io_result_is_error(w)) return w;
+l_Lean_exportAttr = io_result_get_value(w);
+lean::mark_persistent(l_Lean_exportAttr);
+lean::register_constant(lean::mk_const_name(lean::mk_const_name("Lean"), "exportAttr"), l_Lean_exportAttr);
+REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name("Lean"), "getExportNameFor"), 2, lean::get_export_name_for_core);
+REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name("Lean"), "isExport"), 2, l_Lean_isExport___boxed);
+return w;
+}
diff --git a/src/stage0/init/lean/compiler/ir/borrow.cpp b/src/stage0/init/lean/compiler/ir/borrow.cpp
index 5e38f6b7d9..12d8c039bc 100644
--- a/src/stage0/init/lean/compiler/ir/borrow.cpp
+++ b/src/stage0/init/lean/compiler/ir/borrow.cpp
@@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: init.lean.compiler.ir.borrow
-// Imports: init.lean.compiler.export init.lean.compiler.ir.compilerm init.lean.compiler.ir.normids
+// Imports: init.lean.compiler.exportattr init.lean.compiler.ir.compilerm init.lean.compiler.ir.normids
 #include "runtime/object.h"
 #include "runtime/apply.h"
 typedef lean::object obj;    typedef lean::usize  usize;
@@ -24,6 +24,7 @@ obj* nat_sub(obj*, obj*);
 }
 obj* l_HashMapImp_find___at_Lean_IR_Borrow_ApplyParamMap_visitFnBody___main___spec__1(obj*, obj*);
 obj* l_Lean_Format_pretty(obj*, obj*);
+extern obj* l_Lean_Syntax_formatStx___main___closed__5;
 extern obj* l_Lean_IR_JoinPointId_HasToString___closed__1;
 obj* l_Array_mkArray(obj*, obj*, obj*);
 obj* l_Lean_IR_Borrow_ownArgs(obj*, obj*, obj*);
@@ -45,7 +46,6 @@ obj* l_Lean_IR_Borrow_preserveTailCall(obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_IR_Borrow_InitParamMap_visitDecls(obj*, obj*, obj*);
 obj* l_Lean_IR_Borrow_Lean_HasFormat;
 obj* l_Array_miterateAux___main___at_Lean_IR_Borrow_updateParamSet___spec__1___boxed(obj*, obj*, obj*, obj*);
-obj* l_Lean_IR_Borrow_ParamMap_fmt___closed__1;
 obj* l_Lean_IR_Borrow_updateParamMap___boxed(obj*, obj*, obj*);
 obj* l_Lean_IR_Borrow_whileModifingOwnedAux___main___at_Lean_IR_Borrow_collectDecl___main___spec__1(obj*, obj*, obj*, obj*);
 obj* l_Lean_IR_Borrow_ApplyParamMap_visitFnBody___main___boxed(obj*, obj*, obj*);
@@ -54,7 +54,6 @@ obj* l_Nat_mforAux___main___at_Lean_IR_Borrow_ownArgsUsingParams___spec__1___box
 obj* l_Lean_Name_toStringWithSep___main(obj*, obj*);
 obj* l_Lean_IR_Borrow_infer___boxed(obj*, obj*);
 obj* l_Nat_mforAux___main___at_Lean_IR_Borrow_ownParamsUsingArgs___spec__1___boxed(obj*, obj*, obj*, obj*, obj*, obj*);
-obj* l_Lean_IR_Borrow_ParamMap_fmt___closed__2;
 obj* l_RBNode_findCore___main___at_Lean_IR_UniqueIds_checkId___spec__1(obj*, obj*);
 obj* l_Array_uset(obj*, obj*, usize, obj*, obj*);
 obj* l_Lean_IR_Borrow_ownArg(obj*, obj*, obj*);
@@ -69,6 +68,7 @@ uint8 l_Lean_IR_IRType_isObj___main(uint8);
 obj* l_Lean_IR_Borrow_ownArgsIfParam___boxed(obj*, obj*, obj*);
 obj* l_Lean_IR_Borrow_preserveTailCall___boxed(obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_IR_Borrow_whileModifingOwnedAux___main(obj*, obj*, obj*, obj*);
+extern obj* l_Lean_Syntax_formatStx___main___closed__4;
 obj* l_Lean_IR_Borrow_collectDecl___main(obj*, obj*, obj*);
 obj* l_Lean_IR_Borrow_getParamInfo(obj*, obj*, obj*);
 obj* l_Array_mforAux___main___at_Lean_IR_Borrow_InitParamMap_visitDecls___spec__1(obj*, obj*, obj*, obj*);
@@ -494,26 +494,6 @@ goto _start;
 }
 }
 }
-obj* _init_l_Lean_IR_Borrow_ParamMap_fmt___closed__1() {
-_start:
-{
-obj* x_1; obj* x_2; 
-x_1 = lean::mk_string("{");
-x_2 = lean::alloc_cnstr(2, 1, 0);
-lean::cnstr_set(x_2, 0, x_1);
-return x_2;
-}
-}
-obj* _init_l_Lean_IR_Borrow_ParamMap_fmt___closed__2() {
-_start:
-{
-obj* x_1; obj* x_2; 
-x_1 = lean::mk_string("}");
-x_2 = lean::alloc_cnstr(2, 1, 0);
-lean::cnstr_set(x_2, 0, x_1);
-return x_2;
-}
-}
 obj* l_Lean_IR_Borrow_ParamMap_fmt(obj* x_1) {
 _start:
 {
@@ -527,12 +507,12 @@ x_7 = lean::alloc_cnstr(3, 2, 0);
 lean::cnstr_set(x_7, 0, x_6);
 lean::cnstr_set(x_7, 1, x_5);
 x_8 = 0;
-x_9 = l_Lean_IR_Borrow_ParamMap_fmt___closed__1;
+x_9 = l_Lean_Syntax_formatStx___main___closed__4;
 x_10 = lean::alloc_cnstr(4, 2, 1);
 lean::cnstr_set(x_10, 0, x_9);
 lean::cnstr_set(x_10, 1, x_7);
 lean::cnstr_set_scalar(x_10, sizeof(void*)*2, x_8);
-x_11 = l_Lean_IR_Borrow_ParamMap_fmt___closed__2;
+x_11 = l_Lean_Syntax_formatStx___main___closed__5;
 x_12 = lean::alloc_cnstr(4, 2, 1);
 lean::cnstr_set(x_12, 0, x_10);
 lean::cnstr_set(x_12, 1, x_11);
@@ -1112,6 +1092,7 @@ lean::inc(x_13);
 x_14 = lean::cnstr_get(x_9, 2);
 lean::inc(x_14);
 lean::dec(x_9);
+lean::inc(x_12);
 x_15 = l_Lean_isExport(x_1, x_12);
 lean::inc(x_12);
 x_16 = lean::alloc_cnstr(0, 1, 0);
@@ -3902,7 +3883,7 @@ lean::dec(x_2);
 return x_4;
 }
 }
-obj* initialize_init_lean_compiler_export(obj*);
+obj* initialize_init_lean_compiler_exportattr(obj*);
 obj* initialize_init_lean_compiler_ir_compilerm(obj*);
 obj* initialize_init_lean_compiler_ir_normids(obj*);
 static bool _G_initialized = false;
@@ -3910,7 +3891,7 @@ obj* initialize_init_lean_compiler_ir_borrow(obj* w) {
 if (_G_initialized) return w;
 _G_initialized = true;
 if (io_result_is_error(w)) return w;
-w = initialize_init_lean_compiler_export(w);
+w = initialize_init_lean_compiler_exportattr(w);
 if (io_result_is_error(w)) return w;
 w = initialize_init_lean_compiler_ir_compilerm(w);
 if (io_result_is_error(w)) return w;
@@ -3928,10 +3909,6 @@ l_AssocList_mfoldl___main___at_Lean_IR_Borrow_ParamMap_fmt___spec__1___closed__1
 lean::mark_persistent(l_AssocList_mfoldl___main___at_Lean_IR_Borrow_ParamMap_fmt___spec__1___closed__1);
 l_AssocList_mfoldl___main___at_Lean_IR_Borrow_ParamMap_fmt___spec__1___closed__2 = _init_l_AssocList_mfoldl___main___at_Lean_IR_Borrow_ParamMap_fmt___spec__1___closed__2();
 lean::mark_persistent(l_AssocList_mfoldl___main___at_Lean_IR_Borrow_ParamMap_fmt___spec__1___closed__2);
-l_Lean_IR_Borrow_ParamMap_fmt___closed__1 = _init_l_Lean_IR_Borrow_ParamMap_fmt___closed__1();
-lean::mark_persistent(l_Lean_IR_Borrow_ParamMap_fmt___closed__1);
-l_Lean_IR_Borrow_ParamMap_fmt___closed__2 = _init_l_Lean_IR_Borrow_ParamMap_fmt___closed__2();
-lean::mark_persistent(l_Lean_IR_Borrow_ParamMap_fmt___closed__2);
 REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name(lean::mk_const_name(lean::mk_const_name(lean::mk_const_name("Lean"), "IR"), "Borrow"), "ParamMap"), "fmt"), 1, l_Lean_IR_Borrow_ParamMap_fmt___boxed);
 l_Lean_IR_Borrow_Lean_HasFormat = _init_l_Lean_IR_Borrow_Lean_HasFormat();
 lean::mark_persistent(l_Lean_IR_Borrow_Lean_HasFormat);
diff --git a/src/stage0/init/lean/compiler/ir/emitcpp.cpp b/src/stage0/init/lean/compiler/ir/emitcpp.cpp
index e12b0ef663..786ff444e0 100644
--- a/src/stage0/init/lean/compiler/ir/emitcpp.cpp
+++ b/src/stage0/init/lean/compiler/ir/emitcpp.cpp
@@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: init.lean.compiler.ir.emitcpp
-// Imports: init.control.conditional init.lean.runtime init.lean.name_mangling init.lean.compiler.export init.lean.compiler.initattr init.lean.compiler.ir.compilerm init.lean.compiler.ir.emitutil init.lean.compiler.ir.normids init.lean.compiler.ir.simpcase init.lean.compiler.ir.boxing
+// Imports: init.control.conditional init.lean.runtime init.lean.name_mangling init.lean.compiler.exportattr init.lean.compiler.initattr init.lean.compiler.ir.compilerm init.lean.compiler.ir.emitutil init.lean.compiler.ir.normids init.lean.compiler.ir.simpcase init.lean.compiler.ir.boxing
 #include "runtime/object.h"
 #include "runtime/apply.h"
 typedef lean::object obj;    typedef lean::usize  usize;
@@ -85,7 +85,6 @@ obj* l_HashMapImp_find___at_Lean_IR_EmitCpp_isObj___spec__1___boxed(obj*, obj*);
 obj* l_Lean_IR_EmitCpp_emitDel___boxed(obj*, obj*, obj*);
 obj* l_Lean_IR_EmitCpp_emit___rarg(obj*, obj*, obj*, obj*);
 extern obj* l_Char_quoteCore___closed__3;
-extern "C" obj* lean_get_export_name_for(obj*, obj*);
 obj* l_Lean_IR_EmitCpp_emitBlock___main___closed__1;
 obj* l_Lean_IR_EmitCpp_openNamespacesAux___boxed(obj*, obj*, obj*);
 obj* l_Nat_mforAux___main___at_Lean_IR_EmitCpp_emitTailCall___spec__3(obj*, obj*, obj*, obj*, obj*, obj*);
@@ -338,6 +337,7 @@ obj* l_Lean_IR_EmitCpp_toCppInitName___closed__1;
 obj* l_Lean_IR_EmitCpp_emitVDecl___boxed(obj*, obj*, obj*, obj*, obj*);
 obj* l_Nat_mforAux___main___at_Lean_IR_EmitCpp_emitReset___spec__1___boxed(obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_IR_EmitCpp_declareVars___boxed(obj*, obj*, obj*, obj*);
+obj* l_Lean_ParametricAttribute_getParam___at_Lean_isIOUnitInitFn___spec__1(obj*, obj*, obj*);
 obj* l_Lean_IR_EmitCpp_emitDeclInit___closed__7;
 obj* l_Lean_IR_EmitCpp_emitArg(obj*, obj*, obj*);
 obj* l_Lean_IR_EmitCpp_emitInc___closed__3;
@@ -368,6 +368,7 @@ obj* l_Lean_IR_EmitCpp_emitCtor(obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_IR_EmitCpp_emitInitFn(obj*, obj*);
 obj* l_Lean_IR_AltCore_body___main(obj*);
 obj* l_Lean_IR_EmitCpp_emitLns___rarg(obj*, obj*, obj*, obj*);
+extern obj* l_Lean_exportAttr;
 uint8 l_Lean_IR_ExplicitBoxing_requiresBoxedVersion(obj*, obj*);
 obj* l_Lean_IR_EmitCpp_toCppInitName(obj*, obj*, obj*);
 obj* l_Lean_IR_EmitCpp_emitOffset___boxed(obj*, obj*, obj*, obj*);
@@ -1401,92 +1402,95 @@ uint8 x_5;
 x_5 = !lean::is_exclusive(x_4);
 if (x_5 == 0)
 {
-obj* x_6; obj* x_7; obj* x_8; obj* x_9; 
+obj* x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_10; 
 x_6 = lean::cnstr_get(x_4, 0);
 x_7 = lean::cnstr_get(x_4, 1);
 x_8 = lean::box(0);
 lean::inc(x_7);
 lean::cnstr_set(x_4, 0, x_8);
-x_9 = lean_get_export_name_for(x_6, x_1);
+x_9 = l_Lean_exportAttr;
+x_10 = l_Lean_ParametricAttribute_getParam___at_Lean_isIOUnitInitFn___spec__1(x_9, x_6, x_1);
 lean::dec(x_6);
-if (lean::obj_tag(x_9) == 0)
+if (lean::obj_tag(x_10) == 0)
 {
-obj* x_10; 
+obj* x_11; 
 lean::dec(x_4);
-x_10 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_10, 0, x_8);
-lean::cnstr_set(x_10, 1, x_7);
-return x_10;
+x_11 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_11, 0, x_8);
+lean::cnstr_set(x_11, 1, x_7);
+return x_11;
 }
 else
 {
-obj* x_11; obj* x_12; 
+obj* x_12; obj* x_13; 
 lean::dec(x_7);
-x_11 = lean::cnstr_get(x_9, 0);
-lean::inc(x_11);
-lean::dec(x_9);
-x_12 = l_Lean_IR_EmitCpp_openNamespaces(x_11, x_2, x_4);
-lean::dec(x_11);
-return x_12;
+x_12 = lean::cnstr_get(x_10, 0);
+lean::inc(x_12);
+lean::dec(x_10);
+x_13 = l_Lean_IR_EmitCpp_openNamespaces(x_12, x_2, x_4);
+lean::dec(x_12);
+return x_13;
 }
 }
 else
 {
-obj* x_13; obj* x_14; obj* x_15; obj* x_16; obj* x_17; 
-x_13 = lean::cnstr_get(x_4, 0);
-x_14 = lean::cnstr_get(x_4, 1);
+obj* x_14; obj* x_15; obj* x_16; obj* x_17; obj* x_18; obj* x_19; 
+x_14 = lean::cnstr_get(x_4, 0);
+x_15 = lean::cnstr_get(x_4, 1);
+lean::inc(x_15);
 lean::inc(x_14);
-lean::inc(x_13);
 lean::dec(x_4);
-x_15 = lean::box(0);
-lean::inc(x_14);
-x_16 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_16, 0, x_15);
-lean::cnstr_set(x_16, 1, x_14);
-x_17 = lean_get_export_name_for(x_13, x_1);
-lean::dec(x_13);
-if (lean::obj_tag(x_17) == 0)
-{
-obj* x_18; 
-lean::dec(x_16);
-x_18 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_18, 0, x_15);
-lean::cnstr_set(x_18, 1, x_14);
-return x_18;
-}
-else
-{
-obj* x_19; obj* x_20; 
+x_16 = lean::box(0);
+lean::inc(x_15);
+x_17 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_17, 0, x_16);
+lean::cnstr_set(x_17, 1, x_15);
+x_18 = l_Lean_exportAttr;
+x_19 = l_Lean_ParametricAttribute_getParam___at_Lean_isIOUnitInitFn___spec__1(x_18, x_14, x_1);
 lean::dec(x_14);
-x_19 = lean::cnstr_get(x_17, 0);
-lean::inc(x_19);
+if (lean::obj_tag(x_19) == 0)
+{
+obj* x_20; 
 lean::dec(x_17);
-x_20 = l_Lean_IR_EmitCpp_openNamespaces(x_19, x_2, x_16);
-lean::dec(x_19);
+x_20 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_20, 0, x_16);
+lean::cnstr_set(x_20, 1, x_15);
 return x_20;
 }
+else
+{
+obj* x_21; obj* x_22; 
+lean::dec(x_15);
+x_21 = lean::cnstr_get(x_19, 0);
+lean::inc(x_21);
+lean::dec(x_19);
+x_22 = l_Lean_IR_EmitCpp_openNamespaces(x_21, x_2, x_17);
+lean::dec(x_21);
+return x_22;
+}
 }
 }
 else
 {
-uint8 x_21; 
-x_21 = !lean::is_exclusive(x_4);
-if (x_21 == 0)
+uint8 x_23; 
+lean::dec(x_1);
+x_23 = !lean::is_exclusive(x_4);
+if (x_23 == 0)
 {
 return x_4;
 }
 else
 {
-obj* x_22; obj* x_23; obj* x_24; 
-x_22 = lean::cnstr_get(x_4, 0);
-x_23 = lean::cnstr_get(x_4, 1);
-lean::inc(x_23);
-lean::inc(x_22);
+obj* x_24; obj* x_25; obj* x_26; 
+x_24 = lean::cnstr_get(x_4, 0);
+x_25 = lean::cnstr_get(x_4, 1);
+lean::inc(x_25);
+lean::inc(x_24);
 lean::dec(x_4);
-x_24 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_24, 0, x_22);
-lean::cnstr_set(x_24, 1, x_23);
-return x_24;
+x_26 = lean::alloc_cnstr(1, 2, 0);
+lean::cnstr_set(x_26, 0, x_24);
+lean::cnstr_set(x_26, 1, x_25);
+return x_26;
 }
 }
 }
@@ -1497,7 +1501,6 @@ _start:
 obj* x_4; 
 x_4 = l_Lean_IR_EmitCpp_openNamespacesFor(x_1, x_2, x_3);
 lean::dec(x_2);
-lean::dec(x_1);
 return x_4;
 }
 }
@@ -1679,92 +1682,95 @@ uint8 x_5;
 x_5 = !lean::is_exclusive(x_4);
 if (x_5 == 0)
 {
-obj* x_6; obj* x_7; obj* x_8; obj* x_9; 
+obj* x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_10; 
 x_6 = lean::cnstr_get(x_4, 0);
 x_7 = lean::cnstr_get(x_4, 1);
 x_8 = lean::box(0);
 lean::inc(x_7);
 lean::cnstr_set(x_4, 0, x_8);
-x_9 = lean_get_export_name_for(x_6, x_1);
+x_9 = l_Lean_exportAttr;
+x_10 = l_Lean_ParametricAttribute_getParam___at_Lean_isIOUnitInitFn___spec__1(x_9, x_6, x_1);
 lean::dec(x_6);
-if (lean::obj_tag(x_9) == 0)
+if (lean::obj_tag(x_10) == 0)
 {
-obj* x_10; 
+obj* x_11; 
 lean::dec(x_4);
-x_10 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_10, 0, x_8);
-lean::cnstr_set(x_10, 1, x_7);
-return x_10;
+x_11 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_11, 0, x_8);
+lean::cnstr_set(x_11, 1, x_7);
+return x_11;
 }
 else
 {
-obj* x_11; obj* x_12; 
+obj* x_12; obj* x_13; 
 lean::dec(x_7);
-x_11 = lean::cnstr_get(x_9, 0);
-lean::inc(x_11);
-lean::dec(x_9);
-x_12 = l_Lean_IR_EmitCpp_closeNamespaces(x_11, x_2, x_4);
-lean::dec(x_11);
-return x_12;
+x_12 = lean::cnstr_get(x_10, 0);
+lean::inc(x_12);
+lean::dec(x_10);
+x_13 = l_Lean_IR_EmitCpp_closeNamespaces(x_12, x_2, x_4);
+lean::dec(x_12);
+return x_13;
 }
 }
 else
 {
-obj* x_13; obj* x_14; obj* x_15; obj* x_16; obj* x_17; 
-x_13 = lean::cnstr_get(x_4, 0);
-x_14 = lean::cnstr_get(x_4, 1);
+obj* x_14; obj* x_15; obj* x_16; obj* x_17; obj* x_18; obj* x_19; 
+x_14 = lean::cnstr_get(x_4, 0);
+x_15 = lean::cnstr_get(x_4, 1);
+lean::inc(x_15);
 lean::inc(x_14);
-lean::inc(x_13);
 lean::dec(x_4);
-x_15 = lean::box(0);
-lean::inc(x_14);
-x_16 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_16, 0, x_15);
-lean::cnstr_set(x_16, 1, x_14);
-x_17 = lean_get_export_name_for(x_13, x_1);
-lean::dec(x_13);
-if (lean::obj_tag(x_17) == 0)
-{
-obj* x_18; 
-lean::dec(x_16);
-x_18 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_18, 0, x_15);
-lean::cnstr_set(x_18, 1, x_14);
-return x_18;
-}
-else
-{
-obj* x_19; obj* x_20; 
+x_16 = lean::box(0);
+lean::inc(x_15);
+x_17 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_17, 0, x_16);
+lean::cnstr_set(x_17, 1, x_15);
+x_18 = l_Lean_exportAttr;
+x_19 = l_Lean_ParametricAttribute_getParam___at_Lean_isIOUnitInitFn___spec__1(x_18, x_14, x_1);
 lean::dec(x_14);
-x_19 = lean::cnstr_get(x_17, 0);
-lean::inc(x_19);
+if (lean::obj_tag(x_19) == 0)
+{
+obj* x_20; 
 lean::dec(x_17);
-x_20 = l_Lean_IR_EmitCpp_closeNamespaces(x_19, x_2, x_16);
-lean::dec(x_19);
+x_20 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_20, 0, x_16);
+lean::cnstr_set(x_20, 1, x_15);
 return x_20;
 }
+else
+{
+obj* x_21; obj* x_22; 
+lean::dec(x_15);
+x_21 = lean::cnstr_get(x_19, 0);
+lean::inc(x_21);
+lean::dec(x_19);
+x_22 = l_Lean_IR_EmitCpp_closeNamespaces(x_21, x_2, x_17);
+lean::dec(x_21);
+return x_22;
+}
 }
 }
 else
 {
-uint8 x_21; 
-x_21 = !lean::is_exclusive(x_4);
-if (x_21 == 0)
+uint8 x_23; 
+lean::dec(x_1);
+x_23 = !lean::is_exclusive(x_4);
+if (x_23 == 0)
 {
 return x_4;
 }
 else
 {
-obj* x_22; obj* x_23; obj* x_24; 
-x_22 = lean::cnstr_get(x_4, 0);
-x_23 = lean::cnstr_get(x_4, 1);
-lean::inc(x_23);
-lean::inc(x_22);
+obj* x_24; obj* x_25; obj* x_26; 
+x_24 = lean::cnstr_get(x_4, 0);
+x_25 = lean::cnstr_get(x_4, 1);
+lean::inc(x_25);
+lean::inc(x_24);
 lean::dec(x_4);
-x_24 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_24, 0, x_22);
-lean::cnstr_set(x_24, 1, x_23);
-return x_24;
+x_26 = lean::alloc_cnstr(1, 2, 0);
+lean::cnstr_set(x_26, 0, x_24);
+lean::cnstr_set(x_26, 1, x_25);
+return x_26;
 }
 }
 }
@@ -1775,7 +1781,6 @@ _start:
 obj* x_4; 
 x_4 = l_Lean_IR_EmitCpp_closeNamespacesFor(x_1, x_2, x_3);
 lean::dec(x_2);
-lean::dec(x_1);
 return x_4;
 }
 }
@@ -1874,155 +1879,159 @@ uint8 x_5;
 x_5 = !lean::is_exclusive(x_4);
 if (x_5 == 0)
 {
-obj* x_6; obj* x_7; obj* x_8; obj* x_9; 
+obj* x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_10; 
 x_6 = lean::cnstr_get(x_4, 0);
 x_7 = lean::cnstr_get(x_4, 1);
 x_8 = lean::box(0);
 lean::inc(x_7);
 lean::cnstr_set(x_4, 0, x_8);
-x_9 = lean_get_export_name_for(x_6, x_1);
+x_9 = l_Lean_exportAttr;
+lean::inc(x_1);
+x_10 = l_Lean_ParametricAttribute_getParam___at_Lean_isIOUnitInitFn___spec__1(x_9, x_6, x_1);
 lean::dec(x_6);
-if (lean::obj_tag(x_9) == 0)
+if (lean::obj_tag(x_10) == 0)
 {
-obj* x_10; uint8 x_11; 
+obj* x_11; uint8 x_12; 
 lean::dec(x_4);
-x_10 = l_Lean_IR_EmitCpp_toBaseCppName___closed__1;
-x_11 = lean_name_dec_eq(x_1, x_10);
-if (x_11 == 0)
+x_11 = l_Lean_IR_EmitCpp_toBaseCppName___closed__1;
+x_12 = lean_name_dec_eq(x_1, x_11);
+if (x_12 == 0)
 {
-obj* x_12; obj* x_13; obj* x_14; 
-x_12 = l_Lean_IR_EmitCpp_toBaseCppName___closed__2;
-x_13 = l_Lean_Name_mangle(x_1, x_12);
-x_14 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_14, 0, x_13);
-lean::cnstr_set(x_14, 1, x_7);
-return x_14;
+obj* x_13; obj* x_14; obj* x_15; 
+x_13 = l_Lean_IR_EmitCpp_toBaseCppName___closed__2;
+x_14 = l_Lean_Name_mangle(x_1, x_13);
+x_15 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_15, 0, x_14);
+lean::cnstr_set(x_15, 1, x_7);
+return x_15;
 }
 else
 {
-obj* x_15; obj* x_16; 
+obj* x_16; obj* x_17; 
 lean::dec(x_1);
-x_15 = l_Lean_IR_EmitCpp_leanMainFn;
-x_16 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_16, 0, x_15);
-lean::cnstr_set(x_16, 1, x_7);
-return x_16;
+x_16 = l_Lean_IR_EmitCpp_leanMainFn;
+x_17 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_17, 0, x_16);
+lean::cnstr_set(x_17, 1, x_7);
+return x_17;
 }
 }
 else
 {
-obj* x_17; 
-x_17 = lean::cnstr_get(x_9, 0);
-lean::inc(x_17);
-lean::dec(x_9);
-switch (lean::obj_tag(x_17)) {
-case 0:
-{
 obj* x_18; 
-lean::dec(x_7);
-x_18 = l_Lean_IR_EmitCpp_throwInvalidExportName___rarg(x_1, x_2, x_4);
-return x_18;
-}
-case 1:
-{
-obj* x_19; obj* x_20; 
-lean::dec(x_4);
-lean::dec(x_1);
-x_19 = lean::cnstr_get(x_17, 1);
-lean::inc(x_19);
-lean::dec(x_17);
-x_20 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_20, 0, x_19);
-lean::cnstr_set(x_20, 1, x_7);
-return x_20;
-}
-default: 
-{
-obj* x_21; 
-lean::dec(x_17);
-lean::dec(x_7);
-x_21 = l_Lean_IR_EmitCpp_throwInvalidExportName___rarg(x_1, x_2, x_4);
-return x_21;
-}
-}
-}
-}
-else
-{
-obj* x_22; obj* x_23; obj* x_24; obj* x_25; obj* x_26; 
-x_22 = lean::cnstr_get(x_4, 0);
-x_23 = lean::cnstr_get(x_4, 1);
-lean::inc(x_23);
-lean::inc(x_22);
-lean::dec(x_4);
-x_24 = lean::box(0);
-lean::inc(x_23);
-x_25 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_25, 0, x_24);
-lean::cnstr_set(x_25, 1, x_23);
-x_26 = lean_get_export_name_for(x_22, x_1);
-lean::dec(x_22);
-if (lean::obj_tag(x_26) == 0)
-{
-obj* x_27; uint8 x_28; 
-lean::dec(x_25);
-x_27 = l_Lean_IR_EmitCpp_toBaseCppName___closed__1;
-x_28 = lean_name_dec_eq(x_1, x_27);
-if (x_28 == 0)
-{
-obj* x_29; obj* x_30; obj* x_31; 
-x_29 = l_Lean_IR_EmitCpp_toBaseCppName___closed__2;
-x_30 = l_Lean_Name_mangle(x_1, x_29);
-x_31 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_31, 0, x_30);
-lean::cnstr_set(x_31, 1, x_23);
-return x_31;
-}
-else
-{
-obj* x_32; obj* x_33; 
-lean::dec(x_1);
-x_32 = l_Lean_IR_EmitCpp_leanMainFn;
-x_33 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_33, 0, x_32);
-lean::cnstr_set(x_33, 1, x_23);
-return x_33;
-}
-}
-else
-{
-obj* x_34; 
-x_34 = lean::cnstr_get(x_26, 0);
-lean::inc(x_34);
-lean::dec(x_26);
-switch (lean::obj_tag(x_34)) {
+x_18 = lean::cnstr_get(x_10, 0);
+lean::inc(x_18);
+lean::dec(x_10);
+switch (lean::obj_tag(x_18)) {
 case 0:
 {
-obj* x_35; 
-lean::dec(x_23);
-x_35 = l_Lean_IR_EmitCpp_throwInvalidExportName___rarg(x_1, x_2, x_25);
-return x_35;
+obj* x_19; 
+lean::dec(x_7);
+x_19 = l_Lean_IR_EmitCpp_throwInvalidExportName___rarg(x_1, x_2, x_4);
+return x_19;
 }
 case 1:
 {
-obj* x_36; obj* x_37; 
-lean::dec(x_25);
+obj* x_20; obj* x_21; 
+lean::dec(x_4);
 lean::dec(x_1);
-x_36 = lean::cnstr_get(x_34, 1);
-lean::inc(x_36);
-lean::dec(x_34);
-x_37 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_37, 0, x_36);
-lean::cnstr_set(x_37, 1, x_23);
-return x_37;
+x_20 = lean::cnstr_get(x_18, 1);
+lean::inc(x_20);
+lean::dec(x_18);
+x_21 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_21, 0, x_20);
+lean::cnstr_set(x_21, 1, x_7);
+return x_21;
 }
 default: 
 {
-obj* x_38; 
-lean::dec(x_34);
+obj* x_22; 
+lean::dec(x_18);
+lean::dec(x_7);
+x_22 = l_Lean_IR_EmitCpp_throwInvalidExportName___rarg(x_1, x_2, x_4);
+return x_22;
+}
+}
+}
+}
+else
+{
+obj* x_23; obj* x_24; obj* x_25; obj* x_26; obj* x_27; obj* x_28; 
+x_23 = lean::cnstr_get(x_4, 0);
+x_24 = lean::cnstr_get(x_4, 1);
+lean::inc(x_24);
+lean::inc(x_23);
+lean::dec(x_4);
+x_25 = lean::box(0);
+lean::inc(x_24);
+x_26 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_26, 0, x_25);
+lean::cnstr_set(x_26, 1, x_24);
+x_27 = l_Lean_exportAttr;
+lean::inc(x_1);
+x_28 = l_Lean_ParametricAttribute_getParam___at_Lean_isIOUnitInitFn___spec__1(x_27, x_23, x_1);
 lean::dec(x_23);
-x_38 = l_Lean_IR_EmitCpp_throwInvalidExportName___rarg(x_1, x_2, x_25);
-return x_38;
+if (lean::obj_tag(x_28) == 0)
+{
+obj* x_29; uint8 x_30; 
+lean::dec(x_26);
+x_29 = l_Lean_IR_EmitCpp_toBaseCppName___closed__1;
+x_30 = lean_name_dec_eq(x_1, x_29);
+if (x_30 == 0)
+{
+obj* x_31; obj* x_32; obj* x_33; 
+x_31 = l_Lean_IR_EmitCpp_toBaseCppName___closed__2;
+x_32 = l_Lean_Name_mangle(x_1, x_31);
+x_33 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_33, 0, x_32);
+lean::cnstr_set(x_33, 1, x_24);
+return x_33;
+}
+else
+{
+obj* x_34; obj* x_35; 
+lean::dec(x_1);
+x_34 = l_Lean_IR_EmitCpp_leanMainFn;
+x_35 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_35, 0, x_34);
+lean::cnstr_set(x_35, 1, x_24);
+return x_35;
+}
+}
+else
+{
+obj* x_36; 
+x_36 = lean::cnstr_get(x_28, 0);
+lean::inc(x_36);
+lean::dec(x_28);
+switch (lean::obj_tag(x_36)) {
+case 0:
+{
+obj* x_37; 
+lean::dec(x_24);
+x_37 = l_Lean_IR_EmitCpp_throwInvalidExportName___rarg(x_1, x_2, x_26);
+return x_37;
+}
+case 1:
+{
+obj* x_38; obj* x_39; 
+lean::dec(x_26);
+lean::dec(x_1);
+x_38 = lean::cnstr_get(x_36, 1);
+lean::inc(x_38);
+lean::dec(x_36);
+x_39 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_39, 0, x_38);
+lean::cnstr_set(x_39, 1, x_24);
+return x_39;
+}
+default: 
+{
+obj* x_40; 
+lean::dec(x_36);
+lean::dec(x_24);
+x_40 = l_Lean_IR_EmitCpp_throwInvalidExportName___rarg(x_1, x_2, x_26);
+return x_40;
 }
 }
 }
@@ -2030,25 +2039,25 @@ return x_38;
 }
 else
 {
-uint8 x_39; 
+uint8 x_41; 
 lean::dec(x_1);
-x_39 = !lean::is_exclusive(x_4);
-if (x_39 == 0)
+x_41 = !lean::is_exclusive(x_4);
+if (x_41 == 0)
 {
 return x_4;
 }
 else
 {
-obj* x_40; obj* x_41; obj* x_42; 
-x_40 = lean::cnstr_get(x_4, 0);
-x_41 = lean::cnstr_get(x_4, 1);
-lean::inc(x_41);
-lean::inc(x_40);
+obj* x_42; obj* x_43; obj* x_44; 
+x_42 = lean::cnstr_get(x_4, 0);
+x_43 = lean::cnstr_get(x_4, 1);
+lean::inc(x_43);
+lean::inc(x_42);
 lean::dec(x_4);
-x_42 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_42, 0, x_40);
-lean::cnstr_set(x_42, 1, x_41);
-return x_42;
+x_44 = lean::alloc_cnstr(1, 2, 0);
+lean::cnstr_set(x_44, 0, x_42);
+lean::cnstr_set(x_44, 1, x_43);
+return x_44;
 }
 }
 }
@@ -2081,118 +2090,122 @@ uint8 x_5;
 x_5 = !lean::is_exclusive(x_4);
 if (x_5 == 0)
 {
-obj* x_6; obj* x_7; 
+obj* x_6; obj* x_7; obj* x_8; 
 x_6 = lean::cnstr_get(x_4, 0);
-x_7 = lean_get_export_name_for(x_6, x_1);
+x_7 = l_Lean_exportAttr;
+lean::inc(x_1);
+x_8 = l_Lean_ParametricAttribute_getParam___at_Lean_isIOUnitInitFn___spec__1(x_7, x_6, x_1);
 lean::dec(x_6);
-if (lean::obj_tag(x_7) == 0)
+if (lean::obj_tag(x_8) == 0)
 {
-obj* x_8; uint8 x_9; 
-x_8 = l_Lean_IR_EmitCpp_toBaseCppName___closed__1;
-x_9 = lean_name_dec_eq(x_1, x_8);
-if (x_9 == 0)
+obj* x_9; uint8 x_10; 
+x_9 = l_Lean_IR_EmitCpp_toBaseCppName___closed__1;
+x_10 = lean_name_dec_eq(x_1, x_9);
+if (x_10 == 0)
 {
-obj* x_10; obj* x_11; 
-x_10 = l_Lean_IR_EmitCpp_toBaseCppName___closed__2;
-x_11 = l_Lean_Name_mangle(x_1, x_10);
-lean::cnstr_set(x_4, 0, x_11);
-return x_4;
-}
-else
-{
-obj* x_12; 
-lean::dec(x_1);
-x_12 = l_Lean_IR_EmitCpp_leanMainFn;
+obj* x_11; obj* x_12; 
+x_11 = l_Lean_IR_EmitCpp_toBaseCppName___closed__2;
+x_12 = l_Lean_Name_mangle(x_1, x_11);
 lean::cnstr_set(x_4, 0, x_12);
 return x_4;
 }
-}
 else
 {
-obj* x_13; obj* x_14; obj* x_15; 
+obj* x_13; 
 lean::dec(x_1);
-x_13 = lean::cnstr_get(x_7, 0);
-lean::inc(x_13);
-lean::dec(x_7);
-x_14 = l_Lean_IR_EmitCpp_toCppName___closed__1;
-x_15 = l_Lean_Name_toStringWithSep___main(x_14, x_13);
-lean::cnstr_set(x_4, 0, x_15);
+x_13 = l_Lean_IR_EmitCpp_leanMainFn;
+lean::cnstr_set(x_4, 0, x_13);
 return x_4;
 }
 }
 else
 {
-obj* x_16; obj* x_17; obj* x_18; 
-x_16 = lean::cnstr_get(x_4, 0);
-x_17 = lean::cnstr_get(x_4, 1);
-lean::inc(x_17);
-lean::inc(x_16);
-lean::dec(x_4);
-x_18 = lean_get_export_name_for(x_16, x_1);
-lean::dec(x_16);
-if (lean::obj_tag(x_18) == 0)
-{
-obj* x_19; uint8 x_20; 
-x_19 = l_Lean_IR_EmitCpp_toBaseCppName___closed__1;
-x_20 = lean_name_dec_eq(x_1, x_19);
-if (x_20 == 0)
-{
-obj* x_21; obj* x_22; obj* x_23; 
-x_21 = l_Lean_IR_EmitCpp_toBaseCppName___closed__2;
-x_22 = l_Lean_Name_mangle(x_1, x_21);
-x_23 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_23, 0, x_22);
-lean::cnstr_set(x_23, 1, x_17);
-return x_23;
+obj* x_14; obj* x_15; obj* x_16; 
+lean::dec(x_1);
+x_14 = lean::cnstr_get(x_8, 0);
+lean::inc(x_14);
+lean::dec(x_8);
+x_15 = l_Lean_IR_EmitCpp_toCppName___closed__1;
+x_16 = l_Lean_Name_toStringWithSep___main(x_15, x_14);
+lean::cnstr_set(x_4, 0, x_16);
+return x_4;
+}
 }
 else
 {
-obj* x_24; obj* x_25; 
-lean::dec(x_1);
-x_24 = l_Lean_IR_EmitCpp_leanMainFn;
+obj* x_17; obj* x_18; obj* x_19; obj* x_20; 
+x_17 = lean::cnstr_get(x_4, 0);
+x_18 = lean::cnstr_get(x_4, 1);
+lean::inc(x_18);
+lean::inc(x_17);
+lean::dec(x_4);
+x_19 = l_Lean_exportAttr;
+lean::inc(x_1);
+x_20 = l_Lean_ParametricAttribute_getParam___at_Lean_isIOUnitInitFn___spec__1(x_19, x_17, x_1);
+lean::dec(x_17);
+if (lean::obj_tag(x_20) == 0)
+{
+obj* x_21; uint8 x_22; 
+x_21 = l_Lean_IR_EmitCpp_toBaseCppName___closed__1;
+x_22 = lean_name_dec_eq(x_1, x_21);
+if (x_22 == 0)
+{
+obj* x_23; obj* x_24; obj* x_25; 
+x_23 = l_Lean_IR_EmitCpp_toBaseCppName___closed__2;
+x_24 = l_Lean_Name_mangle(x_1, x_23);
 x_25 = lean::alloc_cnstr(0, 2, 0);
 lean::cnstr_set(x_25, 0, x_24);
-lean::cnstr_set(x_25, 1, x_17);
+lean::cnstr_set(x_25, 1, x_18);
 return x_25;
 }
+else
+{
+obj* x_26; obj* x_27; 
+lean::dec(x_1);
+x_26 = l_Lean_IR_EmitCpp_leanMainFn;
+x_27 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_27, 0, x_26);
+lean::cnstr_set(x_27, 1, x_18);
+return x_27;
+}
 }
 else
 {
-obj* x_26; obj* x_27; obj* x_28; obj* x_29; 
+obj* x_28; obj* x_29; obj* x_30; obj* x_31; 
 lean::dec(x_1);
-x_26 = lean::cnstr_get(x_18, 0);
-lean::inc(x_26);
-lean::dec(x_18);
-x_27 = l_Lean_IR_EmitCpp_toCppName___closed__1;
-x_28 = l_Lean_Name_toStringWithSep___main(x_27, x_26);
-x_29 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_29, 0, x_28);
-lean::cnstr_set(x_29, 1, x_17);
-return x_29;
+x_28 = lean::cnstr_get(x_20, 0);
+lean::inc(x_28);
+lean::dec(x_20);
+x_29 = l_Lean_IR_EmitCpp_toCppName___closed__1;
+x_30 = l_Lean_Name_toStringWithSep___main(x_29, x_28);
+x_31 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_31, 0, x_30);
+lean::cnstr_set(x_31, 1, x_18);
+return x_31;
 }
 }
 }
 else
 {
-uint8 x_30; 
+uint8 x_32; 
 lean::dec(x_1);
-x_30 = !lean::is_exclusive(x_4);
-if (x_30 == 0)
+x_32 = !lean::is_exclusive(x_4);
+if (x_32 == 0)
 {
 return x_4;
 }
 else
 {
-obj* x_31; obj* x_32; obj* x_33; 
-x_31 = lean::cnstr_get(x_4, 0);
-x_32 = lean::cnstr_get(x_4, 1);
-lean::inc(x_32);
-lean::inc(x_31);
+obj* x_33; obj* x_34; obj* x_35; 
+x_33 = lean::cnstr_get(x_4, 0);
+x_34 = lean::cnstr_get(x_4, 1);
+lean::inc(x_34);
+lean::inc(x_33);
 lean::dec(x_4);
-x_33 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_33, 0, x_31);
-lean::cnstr_set(x_33, 1, x_32);
-return x_33;
+x_35 = lean::alloc_cnstr(1, 2, 0);
+lean::cnstr_set(x_35, 0, x_33);
+lean::cnstr_set(x_35, 1, x_34);
+return x_35;
 }
 }
 }
@@ -2296,145 +2309,149 @@ uint8 x_5;
 x_5 = !lean::is_exclusive(x_4);
 if (x_5 == 0)
 {
-obj* x_6; obj* x_7; obj* x_8; obj* x_9; 
+obj* x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_10; 
 x_6 = lean::cnstr_get(x_4, 0);
 x_7 = lean::cnstr_get(x_4, 1);
 x_8 = lean::box(0);
 lean::inc(x_7);
 lean::cnstr_set(x_4, 0, x_8);
-x_9 = lean_get_export_name_for(x_6, x_1);
+x_9 = l_Lean_exportAttr;
+lean::inc(x_1);
+x_10 = l_Lean_ParametricAttribute_getParam___at_Lean_isIOUnitInitFn___spec__1(x_9, x_6, x_1);
 lean::dec(x_6);
-if (lean::obj_tag(x_9) == 0)
+if (lean::obj_tag(x_10) == 0)
 {
-obj* x_10; obj* x_11; obj* x_12; obj* x_13; obj* x_14; 
+obj* x_11; obj* x_12; obj* x_13; obj* x_14; obj* x_15; 
 lean::dec(x_4);
-x_10 = l_Lean_IR_EmitCpp_toBaseCppName___closed__2;
-x_11 = l_Lean_Name_mangle(x_1, x_10);
-x_12 = l_Lean_IR_EmitCpp_toCppInitName___closed__1;
-x_13 = lean::string_append(x_12, x_11);
-lean::dec(x_11);
-x_14 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_14, 0, x_13);
-lean::cnstr_set(x_14, 1, x_7);
-return x_14;
+x_11 = l_Lean_IR_EmitCpp_toBaseCppName___closed__2;
+x_12 = l_Lean_Name_mangle(x_1, x_11);
+x_13 = l_Lean_IR_EmitCpp_toCppInitName___closed__1;
+x_14 = lean::string_append(x_13, x_12);
+lean::dec(x_12);
+x_15 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_15, 0, x_14);
+lean::cnstr_set(x_15, 1, x_7);
+return x_15;
 }
 else
 {
-obj* x_15; 
-x_15 = lean::cnstr_get(x_9, 0);
-lean::inc(x_15);
-lean::dec(x_9);
-switch (lean::obj_tag(x_15)) {
-case 0:
-{
 obj* x_16; 
-lean::dec(x_7);
-x_16 = l_Lean_IR_EmitCpp_throwInvalidExportName___rarg(x_1, x_2, x_4);
-return x_16;
-}
-case 1:
-{
-obj* x_17; obj* x_18; obj* x_19; obj* x_20; obj* x_21; obj* x_22; obj* x_23; obj* x_24; 
-lean::dec(x_4);
-lean::dec(x_1);
-x_17 = lean::cnstr_get(x_15, 0);
-lean::inc(x_17);
-x_18 = lean::cnstr_get(x_15, 1);
-lean::inc(x_18);
-lean::dec(x_15);
-x_19 = l_Lean_IR_EmitCpp_toCppInitName___closed__1;
-x_20 = lean::string_append(x_19, x_18);
-lean::dec(x_18);
-x_21 = lean_name_mk_string(x_17, x_20);
-x_22 = l_Lean_IR_EmitCpp_toCppName___closed__1;
-x_23 = l_Lean_Name_toStringWithSep___main(x_22, x_21);
-x_24 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_24, 0, x_23);
-lean::cnstr_set(x_24, 1, x_7);
-return x_24;
-}
-default: 
-{
-obj* x_25; 
-lean::dec(x_15);
-lean::dec(x_7);
-x_25 = l_Lean_IR_EmitCpp_throwInvalidExportName___rarg(x_1, x_2, x_4);
-return x_25;
-}
-}
-}
-}
-else
-{
-obj* x_26; obj* x_27; obj* x_28; obj* x_29; obj* x_30; 
-x_26 = lean::cnstr_get(x_4, 0);
-x_27 = lean::cnstr_get(x_4, 1);
-lean::inc(x_27);
-lean::inc(x_26);
-lean::dec(x_4);
-x_28 = lean::box(0);
-lean::inc(x_27);
-x_29 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_29, 0, x_28);
-lean::cnstr_set(x_29, 1, x_27);
-x_30 = lean_get_export_name_for(x_26, x_1);
-lean::dec(x_26);
-if (lean::obj_tag(x_30) == 0)
-{
-obj* x_31; obj* x_32; obj* x_33; obj* x_34; obj* x_35; 
-lean::dec(x_29);
-x_31 = l_Lean_IR_EmitCpp_toBaseCppName___closed__2;
-x_32 = l_Lean_Name_mangle(x_1, x_31);
-x_33 = l_Lean_IR_EmitCpp_toCppInitName___closed__1;
-x_34 = lean::string_append(x_33, x_32);
-lean::dec(x_32);
-x_35 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_35, 0, x_34);
-lean::cnstr_set(x_35, 1, x_27);
-return x_35;
-}
-else
-{
-obj* x_36; 
-x_36 = lean::cnstr_get(x_30, 0);
-lean::inc(x_36);
-lean::dec(x_30);
-switch (lean::obj_tag(x_36)) {
+x_16 = lean::cnstr_get(x_10, 0);
+lean::inc(x_16);
+lean::dec(x_10);
+switch (lean::obj_tag(x_16)) {
 case 0:
 {
-obj* x_37; 
-lean::dec(x_27);
-x_37 = l_Lean_IR_EmitCpp_throwInvalidExportName___rarg(x_1, x_2, x_29);
-return x_37;
+obj* x_17; 
+lean::dec(x_7);
+x_17 = l_Lean_IR_EmitCpp_throwInvalidExportName___rarg(x_1, x_2, x_4);
+return x_17;
 }
 case 1:
 {
-obj* x_38; obj* x_39; obj* x_40; obj* x_41; obj* x_42; obj* x_43; obj* x_44; obj* x_45; 
-lean::dec(x_29);
+obj* x_18; obj* x_19; obj* x_20; obj* x_21; obj* x_22; obj* x_23; obj* x_24; obj* x_25; 
+lean::dec(x_4);
 lean::dec(x_1);
-x_38 = lean::cnstr_get(x_36, 0);
-lean::inc(x_38);
-x_39 = lean::cnstr_get(x_36, 1);
-lean::inc(x_39);
-lean::dec(x_36);
-x_40 = l_Lean_IR_EmitCpp_toCppInitName___closed__1;
-x_41 = lean::string_append(x_40, x_39);
-lean::dec(x_39);
-x_42 = lean_name_mk_string(x_38, x_41);
-x_43 = l_Lean_IR_EmitCpp_toCppName___closed__1;
-x_44 = l_Lean_Name_toStringWithSep___main(x_43, x_42);
-x_45 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_45, 0, x_44);
-lean::cnstr_set(x_45, 1, x_27);
-return x_45;
+x_18 = lean::cnstr_get(x_16, 0);
+lean::inc(x_18);
+x_19 = lean::cnstr_get(x_16, 1);
+lean::inc(x_19);
+lean::dec(x_16);
+x_20 = l_Lean_IR_EmitCpp_toCppInitName___closed__1;
+x_21 = lean::string_append(x_20, x_19);
+lean::dec(x_19);
+x_22 = lean_name_mk_string(x_18, x_21);
+x_23 = l_Lean_IR_EmitCpp_toCppName___closed__1;
+x_24 = l_Lean_Name_toStringWithSep___main(x_23, x_22);
+x_25 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_25, 0, x_24);
+lean::cnstr_set(x_25, 1, x_7);
+return x_25;
 }
 default: 
 {
-obj* x_46; 
-lean::dec(x_36);
+obj* x_26; 
+lean::dec(x_16);
+lean::dec(x_7);
+x_26 = l_Lean_IR_EmitCpp_throwInvalidExportName___rarg(x_1, x_2, x_4);
+return x_26;
+}
+}
+}
+}
+else
+{
+obj* x_27; obj* x_28; obj* x_29; obj* x_30; obj* x_31; obj* x_32; 
+x_27 = lean::cnstr_get(x_4, 0);
+x_28 = lean::cnstr_get(x_4, 1);
+lean::inc(x_28);
+lean::inc(x_27);
+lean::dec(x_4);
+x_29 = lean::box(0);
+lean::inc(x_28);
+x_30 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_30, 0, x_29);
+lean::cnstr_set(x_30, 1, x_28);
+x_31 = l_Lean_exportAttr;
+lean::inc(x_1);
+x_32 = l_Lean_ParametricAttribute_getParam___at_Lean_isIOUnitInitFn___spec__1(x_31, x_27, x_1);
 lean::dec(x_27);
-x_46 = l_Lean_IR_EmitCpp_throwInvalidExportName___rarg(x_1, x_2, x_29);
-return x_46;
+if (lean::obj_tag(x_32) == 0)
+{
+obj* x_33; obj* x_34; obj* x_35; obj* x_36; obj* x_37; 
+lean::dec(x_30);
+x_33 = l_Lean_IR_EmitCpp_toBaseCppName___closed__2;
+x_34 = l_Lean_Name_mangle(x_1, x_33);
+x_35 = l_Lean_IR_EmitCpp_toCppInitName___closed__1;
+x_36 = lean::string_append(x_35, x_34);
+lean::dec(x_34);
+x_37 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_37, 0, x_36);
+lean::cnstr_set(x_37, 1, x_28);
+return x_37;
+}
+else
+{
+obj* x_38; 
+x_38 = lean::cnstr_get(x_32, 0);
+lean::inc(x_38);
+lean::dec(x_32);
+switch (lean::obj_tag(x_38)) {
+case 0:
+{
+obj* x_39; 
+lean::dec(x_28);
+x_39 = l_Lean_IR_EmitCpp_throwInvalidExportName___rarg(x_1, x_2, x_30);
+return x_39;
+}
+case 1:
+{
+obj* x_40; obj* x_41; obj* x_42; obj* x_43; obj* x_44; obj* x_45; obj* x_46; obj* x_47; 
+lean::dec(x_30);
+lean::dec(x_1);
+x_40 = lean::cnstr_get(x_38, 0);
+lean::inc(x_40);
+x_41 = lean::cnstr_get(x_38, 1);
+lean::inc(x_41);
+lean::dec(x_38);
+x_42 = l_Lean_IR_EmitCpp_toCppInitName___closed__1;
+x_43 = lean::string_append(x_42, x_41);
+lean::dec(x_41);
+x_44 = lean_name_mk_string(x_40, x_43);
+x_45 = l_Lean_IR_EmitCpp_toCppName___closed__1;
+x_46 = l_Lean_Name_toStringWithSep___main(x_45, x_44);
+x_47 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_47, 0, x_46);
+lean::cnstr_set(x_47, 1, x_28);
+return x_47;
+}
+default: 
+{
+obj* x_48; 
+lean::dec(x_38);
+lean::dec(x_28);
+x_48 = l_Lean_IR_EmitCpp_throwInvalidExportName___rarg(x_1, x_2, x_30);
+return x_48;
 }
 }
 }
@@ -2442,25 +2459,25 @@ return x_46;
 }
 else
 {
-uint8 x_47; 
+uint8 x_49; 
 lean::dec(x_1);
-x_47 = !lean::is_exclusive(x_4);
-if (x_47 == 0)
+x_49 = !lean::is_exclusive(x_4);
+if (x_49 == 0)
 {
 return x_4;
 }
 else
 {
-obj* x_48; obj* x_49; obj* x_50; 
-x_48 = lean::cnstr_get(x_4, 0);
-x_49 = lean::cnstr_get(x_4, 1);
-lean::inc(x_49);
-lean::inc(x_48);
+obj* x_50; obj* x_51; obj* x_52; 
+x_50 = lean::cnstr_get(x_4, 0);
+x_51 = lean::cnstr_get(x_4, 1);
+lean::inc(x_51);
+lean::inc(x_50);
 lean::dec(x_4);
-x_50 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_50, 0, x_48);
-lean::cnstr_set(x_50, 1, x_49);
-return x_50;
+x_52 = lean::alloc_cnstr(1, 2, 0);
+lean::cnstr_set(x_52, 0, x_50);
+lean::cnstr_set(x_52, 1, x_51);
+return x_52;
 }
 }
 }
@@ -2882,6 +2899,7 @@ _start:
 {
 obj* x_5; obj* x_6; 
 x_5 = l_Lean_IR_Decl_name___main(x_1);
+lean::inc(x_5);
 x_6 = l_Lean_IR_EmitCpp_openNamespacesFor(x_5, x_3, x_4);
 if (lean::obj_tag(x_6) == 0)
 {
@@ -2918,7 +2936,6 @@ x_15 = lean::cnstr_get(x_13, 0);
 lean::dec(x_15);
 lean::cnstr_set(x_13, 0, x_9);
 x_16 = l_Lean_IR_EmitCpp_closeNamespacesFor(x_5, x_3, x_13);
-lean::dec(x_5);
 return x_16;
 }
 else
@@ -2931,7 +2948,6 @@ x_18 = lean::alloc_cnstr(0, 2, 0);
 lean::cnstr_set(x_18, 0, x_9);
 lean::cnstr_set(x_18, 1, x_17);
 x_19 = l_Lean_IR_EmitCpp_closeNamespacesFor(x_5, x_3, x_18);
-lean::dec(x_5);
 return x_19;
 }
 }
@@ -2993,7 +3009,6 @@ if (lean::is_scalar(x_29)) {
 lean::cnstr_set(x_30, 0, x_9);
 lean::cnstr_set(x_30, 1, x_28);
 x_31 = l_Lean_IR_EmitCpp_closeNamespacesFor(x_5, x_3, x_30);
-lean::dec(x_5);
 return x_31;
 }
 else
@@ -3104,7 +3119,6 @@ if (lean::is_scalar(x_50)) {
 lean::cnstr_set(x_51, 0, x_41);
 lean::cnstr_set(x_51, 1, x_49);
 x_52 = l_Lean_IR_EmitCpp_closeNamespacesFor(x_5, x_3, x_51);
-lean::dec(x_5);
 return x_52;
 }
 else
@@ -22968,6 +22982,7 @@ lean::inc(x_21);
 lean::inc(x_20);
 lean::cnstr_set(x_2, 3, x_11);
 lean::cnstr_set(x_2, 2, x_10);
+lean::inc(x_15);
 x_24 = l_Lean_IR_EmitCpp_openNamespacesFor(x_15, x_2, x_4);
 if (lean::obj_tag(x_24) == 0)
 {
@@ -23226,7 +23241,6 @@ lean::cnstr_set(x_37, 1, x_43);
 lean::cnstr_set(x_37, 0, x_8);
 x_44 = l_Lean_IR_EmitCpp_closeNamespacesFor(x_15, x_2, x_37);
 lean::dec(x_2);
-lean::dec(x_15);
 return x_44;
 }
 else
@@ -23243,7 +23257,6 @@ lean::cnstr_set(x_49, 0, x_8);
 lean::cnstr_set(x_49, 1, x_48);
 x_50 = l_Lean_IR_EmitCpp_closeNamespacesFor(x_15, x_2, x_49);
 lean::dec(x_2);
-lean::dec(x_15);
 return x_50;
 }
 }
@@ -23463,7 +23476,6 @@ lean::cnstr_set(x_131, 0, x_8);
 lean::cnstr_set(x_131, 1, x_130);
 x_132 = l_Lean_IR_EmitCpp_closeNamespacesFor(x_15, x_2, x_131);
 lean::dec(x_2);
-lean::dec(x_15);
 return x_132;
 }
 else
@@ -23549,6 +23561,7 @@ lean::cnstr_set(x_178, 2, x_10);
 lean::cnstr_set(x_178, 3, x_11);
 lean::cnstr_set(x_178, 4, x_176);
 lean::cnstr_set(x_178, 5, x_177);
+lean::inc(x_15);
 x_179 = l_Lean_IR_EmitCpp_openNamespacesFor(x_15, x_178, x_4);
 if (lean::obj_tag(x_179) == 0)
 {
@@ -23751,7 +23764,6 @@ lean::cnstr_set(x_199, 0, x_8);
 lean::cnstr_set(x_199, 1, x_198);
 x_200 = l_Lean_IR_EmitCpp_closeNamespacesFor(x_15, x_178, x_199);
 lean::dec(x_178);
-lean::dec(x_15);
 return x_200;
 }
 else
@@ -23932,6 +23944,7 @@ lean::cnstr_set(x_266, 2, x_252);
 lean::cnstr_set(x_266, 3, x_253);
 lean::cnstr_set(x_266, 4, x_263);
 lean::cnstr_set(x_266, 5, x_264);
+lean::inc(x_257);
 x_267 = l_Lean_IR_EmitCpp_openNamespacesFor(x_257, x_266, x_250);
 if (lean::obj_tag(x_267) == 0)
 {
@@ -24134,7 +24147,6 @@ lean::cnstr_set(x_287, 0, x_249);
 lean::cnstr_set(x_287, 1, x_286);
 x_288 = l_Lean_IR_EmitCpp_closeNamespacesFor(x_257, x_266, x_287);
 lean::dec(x_266);
-lean::dec(x_257);
 return x_288;
 }
 else
@@ -30484,7 +30496,7 @@ return x_12;
 obj* initialize_init_control_conditional(obj*);
 obj* initialize_init_lean_runtime(obj*);
 obj* initialize_init_lean_name__mangling(obj*);
-obj* initialize_init_lean_compiler_export(obj*);
+obj* initialize_init_lean_compiler_exportattr(obj*);
 obj* initialize_init_lean_compiler_initattr(obj*);
 obj* initialize_init_lean_compiler_ir_compilerm(obj*);
 obj* initialize_init_lean_compiler_ir_emitutil(obj*);
@@ -30502,7 +30514,7 @@ w = initialize_init_lean_runtime(w);
 if (io_result_is_error(w)) return w;
 w = initialize_init_lean_name__mangling(w);
 if (io_result_is_error(w)) return w;
-w = initialize_init_lean_compiler_export(w);
+w = initialize_init_lean_compiler_exportattr(w);
 if (io_result_is_error(w)) return w;
 w = initialize_init_lean_compiler_initattr(w);
 if (io_result_is_error(w)) return w;