diff --git a/library/init/lean/compiler/ir/basic.lean b/library/init/lean/compiler/ir/basic.lean
index ff68839a17..f6a423019d 100644
--- a/library/init/lean/compiler/ir/basic.lean
+++ b/library/init/lean/compiler/ir/basic.lean
@@ -340,7 +340,7 @@ bs.hmmap $ λ b, match b with
 
 inductive Decl
 | fdecl  (f : FunId) (xs : Array Param) (ty : IRType) (b : FnBody)
-| extern (f : FunId) (xs : Array Param) (ty : IRType) (ext : ExternEntry)
+| extern (f : FunId) (xs : Array Param) (ty : IRType) (ext : ExternAttrData)
 
 namespace Decl
 
@@ -363,6 +363,9 @@ end Decl
 
 @[export lean.ir.mk_decl_core] def mkDecl (f : FunId) (xs : Array Param) (ty : IRType) (b : FnBody) : Decl := Decl.fdecl f xs ty b
 
+@[export lean.ir.mk_extern_decl_core] def mkExternDecl (f : FunId) (xs : Array Param) (ty : IRType) (e : ExternAttrData) : Decl :=
+Decl.extern f xs ty e
+
 /-- `Expr.isPure e` return `true` Iff `e` is in the `λPure` fragment. -/
 def Expr.isPure : Expr → Bool
 | (Expr.ctor _ _)    := true
diff --git a/library/init/lean/compiler/ir/compilerm.lean b/library/init/lean/compiler/ir/compilerm.lean
index e7ce89aa54..4bc11412fd 100644
--- a/library/init/lean/compiler/ir/compilerm.lean
+++ b/library/init/lean/compiler/ir/compilerm.lean
@@ -103,6 +103,10 @@ def getDecl (n : Name) : CompilerM Decl :=
 do (some decl) ← findDecl n | throw ("unknown declaration '" ++ toString n ++ "'"),
    pure decl
 
+@[export lean.ir.add_decl_core]
+def addDeclAux (env : Environment) (decl : Decl) : Environment :=
+declMapExt.addEntry env decl
+
 def addDecl (decl : Decl) : CompilerM Unit :=
 modifyEnv (λ env, declMapExt.addEntry env decl)
 
diff --git a/src/library/compiler/compiler.cpp b/src/library/compiler/compiler.cpp
index 9acf1372e6..96a3735d3c 100644
--- a/src/library/compiler/compiler.cpp
+++ b/src/library/compiler/compiler.cpp
@@ -28,6 +28,7 @@ Author: Leonardo de Moura
 #include "library/compiler/export_attribute.h"
 #include "library/compiler/extern_attribute.h"
 #include "library/compiler/struct_cases_on.h"
+#include "library/compiler/ir.h"
 
 namespace lean {
 static name * g_codegen = nullptr;
@@ -173,8 +174,9 @@ environment compile(environment const & env, options const & opts, names cs) {
 
     if (length(cs) == 1 && is_extern_constant(env, head(cs))) {
         /* Generate boxed version for extern/native constant if needed. */
+        environment new_env = ir::add_extern(env, head(cs));
         unsigned arity = *get_extern_constant_arity(env, head(cs));
-        if (optional<pair<environment, comp_decl>> p = mk_boxed_version(env, head(cs), arity)) {
+        if (optional<pair<environment, comp_decl>> p = mk_boxed_version(new_env, head(cs), arity)) {
             /* Remark: we don't need boxed version for the bytecode. */
             return save_llnf_code(p->first, comp_decls(p->second));
         } else {
diff --git a/src/library/compiler/extern_attribute.cpp b/src/library/compiler/extern_attribute.cpp
index e2b57092bb..8b1baad6b0 100644
--- a/src/library/compiler/extern_attribute.cpp
+++ b/src/library/compiler/extern_attribute.cpp
@@ -27,7 +27,6 @@ object* get_extern_entry_for_core(object*, object*);
 
 typedef object_ref extern_entry;
 typedef list_ref<extern_entry> extern_entries;
-typedef object_ref extern_attr_data_value;
 
 extern_entry mk_adhoc_ext_entry(name const & backend) {
     inc(backend.raw());
@@ -133,6 +132,15 @@ extern_attr const & get_extern_attr() {
     return static_cast<extern_attr const &>(get_system_attribute("extern"));
 }
 
+optional<extern_attr_data_value> get_extern_attr_data(environment const & env, name const & fn) {
+    if (std::shared_ptr<extern_attr_data> const & data = get_extern_attr().get(env, fn)) {
+        extern_attr_data_value const & v = data->m_value;
+        return optional<extern_attr_data_value>(v);
+    } else {
+        return optional<extern_attr_data_value>();
+    }
+}
+
 optional<std::string> get_extern_name_for(environment const & env, name const & backend, name const & fn) {
     if (std::shared_ptr<extern_attr_data> const & data = get_extern_attr().get(env, fn)) {
         extern_attr_data_value const & v = data->m_value;
diff --git a/src/library/compiler/extern_attribute.h b/src/library/compiler/extern_attribute.h
index 1c9196866f..aace9deafd 100644
--- a/src/library/compiler/extern_attribute.h
+++ b/src/library/compiler/extern_attribute.h
@@ -11,6 +11,8 @@ namespace lean {
 bool is_extern_constant(environment const & env, name const & c);
 optional<expr> get_extern_constant_ll_type(environment const & env, name const & c);
 optional<unsigned> get_extern_constant_arity(environment const & env, name const & c);
+typedef object_ref extern_attr_data_value;
+optional<extern_attr_data_value> get_extern_attr_data(environment const & env, name const & c);
 /* Return true if `c` is an extern constant, and store in borrowed_args and
    borrowed_res which arguments/results are marked as borrowed. */
 bool get_extern_borrowed_info(environment const & env, name const & c, buffer<bool> & borrowed_args, bool & borrowed_res);
diff --git a/src/library/compiler/ir.cpp b/src/library/compiler/ir.cpp
index de1fbe0f64..91efd9564d 100644
--- a/src/library/compiler/ir.cpp
+++ b/src/library/compiler/ir.cpp
@@ -12,6 +12,7 @@ Author: Leonardo de Moura
 #include "library/trace.h"
 #include "library/compiler/util.h"
 #include "library/compiler/llnf.h"
+#include "library/compiler/extern_attribute.h"
 
 namespace lean {
 namespace ir {
@@ -38,9 +39,11 @@ object * mk_jmp_core(object * j, object * ys);
 extern object * mk_unreachable_core;
 object * mk_alt_core(object * n, object * cidx, object * size, object * usize, object * ssize, object * b);
 object * mk_decl_core(object * f, object * xs, uint8 ty, object * b);
+object * mk_extern_decl_core(object * f, object * xs, uint8 ty, object * ext_entry);
 object * decl_to_string_core(object * d);
 object * compile_core(object * env, object * opts, object * decls);
 object * log_to_string_core(object * log);
+object * add_decl_core(object * env, object * decl);
 /*
 inductive IRType
 | float | uint8 | uint16 | uint32 | uint64 | usize
@@ -61,62 +64,57 @@ typedef object_ref decl;
 arg mk_var_arg(var_id const & id) { inc(id.raw()); return arg(mk_var_arg_core(id.raw())); }
 arg mk_irrelevant_arg() { return arg(mk_irrelevant_arg_core); }
 param mk_param(var_id const & x, type ty) {
-    inc(x.raw());
     uint8 borrowed = false;
-    return param(mk_param_core(x.raw(), borrowed, static_cast<uint8>(ty)));
+    return param(mk_param_core(x.to_obj_arg(), borrowed, static_cast<uint8>(ty)));
 }
 expr mk_ctor(name const & n, unsigned cidx, unsigned size, unsigned usize, unsigned ssize, buffer<arg> const & ys) {
-    inc(n.raw());
-    return expr(mk_ctor_expr_core(n.raw(), mk_nat_obj(cidx), mk_nat_obj(size), mk_nat_obj(usize), mk_nat_obj(ssize), to_array(ys)));
+    return expr(mk_ctor_expr_core(n.to_obj_arg(), mk_nat_obj(cidx), mk_nat_obj(size), mk_nat_obj(usize), mk_nat_obj(ssize), to_array(ys)));
 }
-expr mk_proj(unsigned i, var_id const & x) { inc(x.raw()); return expr(mk_proj_expr_core(mk_nat_obj(i), x.raw())); }
-expr mk_uproj(unsigned i, var_id const & x) { inc(x.raw()); return expr(mk_uproj_expr_core(mk_nat_obj(i), x.raw())); }
-expr mk_sproj(unsigned i, unsigned o, var_id const & x) { inc(x.raw()); return expr(mk_sproj_expr_core(mk_nat_obj(i), mk_nat_obj(o), x.raw())); }
-expr mk_fapp(fun_id const & c, buffer<arg> const & ys) { inc(c.raw()); return expr(mk_fapp_expr_core(c.raw(), to_array(ys))); }
-expr mk_papp(fun_id const & c, buffer<arg> const & ys) { inc(c.raw()); return expr(mk_papp_expr_core(c.raw(), to_array(ys))); }
-expr mk_app(var_id const & x, buffer<arg> const & ys) { inc(x.raw()); return expr(mk_app_expr_core(x.raw(), to_array(ys))); }
-expr mk_num_lit(nat const & v) { inc(v.raw()); return expr(mk_num_expr_core(v.raw())); }
-expr mk_str_lit(string_ref const & v) { inc(v.raw()); return expr(mk_str_expr_core(v.raw())); }
+expr mk_proj(unsigned i, var_id const & x) { return expr(mk_proj_expr_core(mk_nat_obj(i), x.to_obj_arg())); }
+expr mk_uproj(unsigned i, var_id const & x) { return expr(mk_uproj_expr_core(mk_nat_obj(i), x.to_obj_arg())); }
+expr mk_sproj(unsigned i, unsigned o, var_id const & x) { return expr(mk_sproj_expr_core(mk_nat_obj(i), mk_nat_obj(o), x.to_obj_arg())); }
+expr mk_fapp(fun_id const & c, buffer<arg> const & ys) { return expr(mk_fapp_expr_core(c.to_obj_arg(), to_array(ys))); }
+expr mk_papp(fun_id const & c, buffer<arg> const & ys) { return expr(mk_papp_expr_core(c.to_obj_arg(), to_array(ys))); }
+expr mk_app(var_id const & x, buffer<arg> const & ys) { return expr(mk_app_expr_core(x.to_obj_arg(), to_array(ys))); }
+expr mk_num_lit(nat const & v) { return expr(mk_num_expr_core(v.to_obj_arg())); }
+expr mk_str_lit(string_ref const & v) { return expr(mk_str_expr_core(v.to_obj_arg())); }
 
 fn_body mk_vdecl(var_id const & x, type ty, expr const & e, fn_body const & b) {
-    inc(x.raw()); inc(e.raw()), inc(b.raw());
-    return fn_body(mk_vdecl_core(x.raw(), static_cast<uint8>(ty), e.raw(), b.raw()));
+    return fn_body(mk_vdecl_core(x.to_obj_arg(), static_cast<uint8>(ty), e.to_obj_arg(), b.to_obj_arg()));
 }
 fn_body mk_jdecl(jp_id const & j, buffer<param> const & xs, expr const & v, fn_body const & b) {
-    inc(j.raw()); inc(v.raw()); inc(b.raw());
-    return fn_body(mk_jdecl_core(j.raw(), to_array(xs), v.raw(), b.raw()));
+    return fn_body(mk_jdecl_core(j.to_obj_arg(), to_array(xs), v.to_obj_arg(), b.to_obj_arg()));
 }
 fn_body mk_uset(var_id const & x, unsigned i, var_id const & y, fn_body const & b) {
-    inc(x.raw()); inc(y.raw()); inc(b.raw());
-    return fn_body(mk_uset_core(x.raw(), mk_nat_obj(i), y.raw(), b.raw()));
+    return fn_body(mk_uset_core(x.to_obj_arg(), mk_nat_obj(i), y.to_obj_arg(), b.to_obj_arg()));
 }
 fn_body mk_sset(var_id const & x, unsigned i, unsigned o, var_id const & y, type ty, fn_body const & b) {
-    inc(x.raw()); inc(y.raw()); inc(b.raw());
-    return fn_body(mk_sset_core(x.raw(), mk_nat_obj(i), mk_nat_obj(o), y.raw(), static_cast<uint8>(ty), b.raw()));
+    return fn_body(mk_sset_core(x.to_obj_arg(), mk_nat_obj(i), mk_nat_obj(o), y.to_obj_arg(), static_cast<uint8>(ty), b.to_obj_arg()));
 }
-fn_body mk_ret(arg const & x) { inc(x.raw()); return fn_body(mk_ret_core(x.raw())); }
+fn_body mk_ret(arg const & x) { return fn_body(mk_ret_core(x.to_obj_arg())); }
 fn_body mk_unreachable() { return fn_body(mk_unreachable_core); }
 alt mk_alt(name const & n, unsigned cidx, unsigned size, unsigned usize, unsigned ssize, fn_body const & b) {
-    inc(n.raw()); inc(b.raw());
-    return alt(mk_alt_core(n.raw(), mk_nat_obj(cidx), mk_nat_obj(size), mk_nat_obj(usize), mk_nat_obj(ssize), b.raw()));
+    return alt(mk_alt_core(n.to_obj_arg(), mk_nat_obj(cidx), mk_nat_obj(size), mk_nat_obj(usize), mk_nat_obj(ssize), b.to_obj_arg()));
 }
 fn_body mk_case(name const & tid, var_id const & x, buffer<alt> const & alts) {
-    inc(tid.raw()); inc(x.raw());
-    return fn_body(mk_case_core(tid.raw(), x.raw(), to_array(alts)));
+    return fn_body(mk_case_core(tid.to_obj_arg(), x.to_obj_arg(), to_array(alts)));
 }
 fn_body mk_jmp(jp_id const & j, buffer<arg> const & ys) {
-    inc(j.raw());
-    return fn_body(mk_jmp_core(j.raw(), to_array(ys)));
+    return fn_body(mk_jmp_core(j.to_obj_arg(), to_array(ys)));
 }
 decl mk_decl(fun_id const & f, buffer<param> const & xs, type ty, fn_body const & b) {
-    inc(f.raw()); inc(b.raw());
-    return decl(mk_decl_core(f.raw(), to_array(xs), static_cast<uint8>(ty), b.raw()));
+    return decl(mk_decl_core(f.to_obj_arg(), to_array(xs), static_cast<uint8>(ty), b.to_obj_arg()));
+}
+decl mk_extern_decl(fun_id const & f, buffer<param> const & xs, type ty, extern_attr_data_value const & v) {
+    return decl(mk_extern_decl_core(f.to_obj_arg(), to_array(xs), static_cast<uint8>(ty), v.to_obj_arg()));
 }
 std::string decl_to_string(decl const & d) {
-    inc(d.raw());
-    string_ref r(decl_to_string_core(d.raw()));
+    string_ref r(decl_to_string_core(d.to_obj_arg()));
     return r.to_std_string();
 }
+environment add_decl(environment const & env, decl const & d) {
+    return environment(add_decl_core(env.to_obj_arg(), d.to_obj_arg()));
+}
 }
 
 class to_ir_fn {
@@ -468,6 +466,22 @@ public:
     to_ir_fn(environment const & env):m_st(env) {}
 
     ir::decl operator()(comp_decl const & d) { return to_ir_decl(d); }
+
+    /* Convert extern constant into a IR.Decl */
+    ir::decl operator()(name const & fn) {
+        lean_assert(is_extern_constant(env(), fn));
+        buffer<ir::param> xs;
+        unsigned arity = *get_extern_constant_arity(env(), fn);
+        expr type      = get_constant_ll_type(env(), fn);
+        for (unsigned i = 0; i < arity; i++) {
+            lean_assert(is_pi(type));
+            xs.push_back(ir::mk_param(ir::var_id(i), to_ir_type(binding_domain(type))));
+            type = binding_body(type);
+        }
+        ir::type result_type = to_ir_type(type);
+        extern_attr_data_value attr = *get_extern_attr_data(env(), fn);
+        return ir::mk_extern_decl(fn, xs, result_type, attr);
+    }
 };
 
 namespace ir {
@@ -503,5 +517,9 @@ environment compile(environment const & env, options const & opts, comp_decls co
         return new_env;
     }
 }
+
+environment add_extern(environment const & env, name const & fn) {
+    return ir::add_decl(env, to_ir_fn(env)(fn));
+}
 }
 }
diff --git a/src/library/compiler/ir.h b/src/library/compiler/ir.h
index 629bf18b9f..03efd71f0d 100644
--- a/src/library/compiler/ir.h
+++ b/src/library/compiler/ir.h
@@ -14,5 +14,6 @@ typedef object_ref decl;
 std::string decl_to_string(decl const & d);
 void test(decl const & d);
 environment compile(environment const & env, options const & opts, comp_decls const & decls);
+environment add_extern(environment const & env, name const & fn);
 }
 }
diff --git a/src/stage0/init/lean/compiler/ir/basic.cpp b/src/stage0/init/lean/compiler/ir/basic.cpp
index cbbebb81dd..fb2ab4e540 100644
--- a/src/stage0/init/lean/compiler/ir/basic.cpp
+++ b/src/stage0/init/lean/compiler/ir/basic.cpp
@@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: init.lean.compiler.ir.basic
-// Imports: init.lean.name init.lean.kvmap init.lean.format init.data.array.default
+// Imports: init.data.array.default init.lean.name init.lean.extern init.lean.kvmap init.lean.format
 #include "runtime/object.h"
 #include "runtime/apply.h"
 typedef lean::object obj;    typedef lean::usize  usize;
@@ -143,6 +143,7 @@ obj* l_Lean_IR_reshape(obj*, obj*);
 obj* l_Lean_IR_JoinPointId_Lean_HasFormat(obj*);
 obj* l_Array_hmmapAux___main___at_Lean_IR_mmodifyJPs___spec__1___rarg___lambda__2(obj*, obj*, obj*, obj*, obj*);
 uint8 l_Array_isEqv___at_Lean_IR_args_alphaEqv___spec__1(obj*, obj*, obj*);
+obj* l_Lean_IR_mkExternDecl___boxed(obj*, obj*, obj*, obj*);
 namespace lean {
 namespace ir {
 obj* mk_case_core(obj*, obj*, obj*);
@@ -180,6 +181,10 @@ obj* nat_add(obj*, obj*);
 }
 obj* l_Array_isEqv___at_Lean_IR_args_alphaEqv___spec__1___boxed(obj*, obj*, obj*);
 uint8 l_Lean_IR_CtorInfo_isScalar(obj*);
+namespace lean {
+namespace ir {
+obj* mk_extern_decl_core(obj*, obj*, uint8, obj*);
+}}
 obj* l_Array_isEqv___at_Lean_IR_FnBody_alphaEqv___main___spec__1___lambda__1___boxed(obj*, obj*, obj*);
 namespace lean {
 uint8 nat_dec_eq(obj*, obj*);
@@ -2567,17 +2572,19 @@ return x_7;
 obj* _init_l_Lean_IR_Decl_Inhabited() {
 _start:
 {
-obj* x_0; obj* x_1; obj* x_2; uint8 x_3; obj* x_4; obj* x_5; 
+obj* x_0; obj* x_1; obj* x_2; uint8 x_3; obj* x_4; obj* x_5; obj* x_6; 
 x_0 = lean::mk_nat_obj(0ul);
 x_1 = lean::mk_empty_array(x_0);
 x_2 = lean::box(0);
 x_3 = 6;
-x_4 = lean::alloc_cnstr(1, 2, 1);
-lean::cnstr_set(x_4, 0, x_2);
-lean::cnstr_set(x_4, 1, x_1);
-lean::cnstr_set_scalar(x_4, sizeof(void*)*2, x_3);
-x_5 = x_4;
-return x_5;
+x_4 = lean::box(12);
+x_5 = lean::alloc_cnstr(0, 3, 1);
+lean::cnstr_set(x_5, 0, x_2);
+lean::cnstr_set(x_5, 1, x_1);
+lean::cnstr_set(x_5, 2, x_4);
+lean::cnstr_set_scalar(x_5, sizeof(void*)*3, x_3);
+x_6 = x_5;
+return x_6;
 }
 }
 obj* l_Lean_IR_Decl_name___main(obj* x_0) {
@@ -2653,19 +2660,10 @@ return x_1;
 uint8 l_Lean_IR_Decl_resultType___main(obj* x_0) {
 _start:
 {
-if (lean::obj_tag(x_0) == 0)
-{
 uint8 x_1; 
 x_1 = lean::cnstr_get_scalar<uint8>(x_0, sizeof(void*)*3);
 return x_1;
 }
-else
-{
-uint8 x_2; 
-x_2 = lean::cnstr_get_scalar<uint8>(x_0, sizeof(void*)*2);
-return x_2;
-}
-}
 }
 obj* l_Lean_IR_Decl_resultType___main___boxed(obj* x_0) {
 _start:
@@ -2720,6 +2718,31 @@ x_5 = lean::ir::mk_decl_core(x_0, x_1, x_4, x_3);
 return x_5;
 }
 }
+namespace lean {
+namespace ir {
+obj* mk_extern_decl_core(obj* x_0, obj* x_1, uint8 x_2, obj* x_3) {
+_start:
+{
+obj* x_4; obj* x_5; 
+x_4 = lean::alloc_cnstr(1, 3, 1);
+lean::cnstr_set(x_4, 0, x_0);
+lean::cnstr_set(x_4, 1, x_1);
+lean::cnstr_set(x_4, 2, x_3);
+lean::cnstr_set_scalar(x_4, sizeof(void*)*3, x_2);
+x_5 = x_4;
+return x_5;
+}
+}
+}}
+obj* l_Lean_IR_mkExternDecl___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+uint8 x_4; obj* x_5; 
+x_4 = lean::unbox(x_2);
+x_5 = lean::ir::mk_extern_decl_core(x_0, x_1, x_4, x_3);
+return x_5;
+}
+}
 uint8 l_Lean_IR_Expr_isPure___main(obj* x_0) {
 _start:
 {
@@ -8064,22 +8087,25 @@ x_0 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_IR_FnBody_beq___boxed),
 return x_0;
 }
 }
+obj* initialize_init_data_array_default(obj*);
 obj* initialize_init_lean_name(obj*);
+obj* initialize_init_lean_extern(obj*);
 obj* initialize_init_lean_kvmap(obj*);
 obj* initialize_init_lean_format(obj*);
-obj* initialize_init_data_array_default(obj*);
 static bool _G_initialized = false;
 obj* initialize_init_lean_compiler_ir_basic(obj* w) {
  if (_G_initialized) return w;
  _G_initialized = true;
 if (io_result_is_error(w)) return w;
+w = initialize_init_data_array_default(w);
+if (io_result_is_error(w)) return w;
 w = initialize_init_lean_name(w);
 if (io_result_is_error(w)) return w;
+w = initialize_init_lean_extern(w);
+if (io_result_is_error(w)) return w;
 w = initialize_init_lean_kvmap(w);
 if (io_result_is_error(w)) return w;
 w = initialize_init_lean_format(w);
-if (io_result_is_error(w)) return w;
-w = initialize_init_data_array_default(w);
 if (io_result_is_error(w)) return w;
  l_Lean_IR_VarId_HasToString___closed__1 = _init_l_Lean_IR_VarId_HasToString___closed__1();
 lean::mark_persistent(l_Lean_IR_VarId_HasToString___closed__1);
diff --git a/src/stage0/init/lean/compiler/ir/compilerm.cpp b/src/stage0/init/lean/compiler/ir/compilerm.cpp
index 956739c034..775b7d766e 100644
--- a/src/stage0/init/lean/compiler/ir/compilerm.cpp
+++ b/src/stage0/init/lean/compiler/ir/compilerm.cpp
@@ -24,10 +24,12 @@ obj* l_RBNode_setBlack___main___rarg(obj*);
 obj* l_Lean_IR_declMapExt___elambda__2___rarg___boxed(obj*, obj*);
 obj* l_Lean_IR_logMessage___rarg(obj*, obj*, obj*, obj*, obj*);
 extern "C" uint8 lean_name_dec_eq(obj*, obj*);
+obj* l_Lean_IR_findDecl_x_27(obj*, obj*, obj*, obj*);
 obj* l_Lean_IR_containsDecl(obj*, obj*, obj*);
 obj* l_Lean_IR_LogEntry_fmt___main(obj*);
 extern obj* l_Array_empty___closed__1;
 obj* l_Lean_IR_logMessage___boxed(obj*);
+obj* l_Array_mfindAux___main___at_Lean_IR_findDecl_x_27___spec__1___boxed(obj*, obj*, obj*);
 obj* l_Lean_Format_pretty(obj*, obj*);
 obj* l_Lean_IR_mkDeclMapExtension___closed__1;
 extern obj* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__2;
@@ -68,6 +70,7 @@ obj* l_Lean_registerPersistentEnvExtensionUnsafe___at_Lean_IR_mkDeclMapExtension
 obj* l_Lean_IR_log(obj*, obj*, obj*);
 obj* l_Lean_IR_mkDeclMapExtension(obj*);
 obj* l_Lean_IR_tracePrefixOptionName;
+obj* l_Array_anyMAux___main___at_Lean_IR_containsDecl_x_27___spec__1___boxed(obj*, obj*, obj*);
 extern "C" usize lean_name_hash_usize(obj*);
 extern obj* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
 obj* l_Lean_PersistentEnvExtension_getState___rarg(obj*, obj*);
@@ -91,6 +94,10 @@ uint8 nat_dec_lt(obj*, obj*);
 obj* l_Array_miterateAux___main___at___private_init_lean_compiler_ir_compilerm_4__mkEntryArray___spec__10___boxed(obj*, obj*, obj*, obj*);
 obj* l_Lean_IR_logDecls(obj*, obj*, obj*, obj*);
 extern obj* l_Char_HasRepr___closed__1;
+namespace lean {
+namespace ir {
+obj* add_decl_core(obj*, obj*);
+}}
 obj* l_Lean_SMap_empty___at_Lean_IR_mkDeclMapExtension___spec__1;
 obj* l_Lean_IR_declMapExt;
 obj* l_AssocList_contains___main___at___private_init_lean_compiler_ir_compilerm_4__mkEntryArray___spec__3___boxed(obj*, obj*);
@@ -111,11 +118,13 @@ obj* l_Lean_IR_LogEntry_fmt(obj*);
 obj* l___private_init_lean_compiler_ir_compilerm_3__logMessageIfAux___rarg___boxed(obj*, obj*, obj*, obj*, obj*);
 uint8 l_AssocList_contains___main___at___private_init_lean_compiler_ir_compilerm_4__mkEntryArray___spec__3(obj*, obj*);
 obj* l_Array_mforAux___main___at_Lean_IR_addDecls___spec__1(obj*, obj*, obj*, obj*);
+obj* l_Array_mfindAux___main___at_Lean_IR_findDecl_x_27___spec__1(obj*, obj*, obj*);
 uint8 l___private_init_lean_compiler_ir_compilerm_1__isLogEnabledFor(obj*, obj*);
 obj* l_RBNode_ins___main___at_Lean_IR_mkDeclMapExtension___spec__5(obj*, obj*, obj*);
 obj* l_Array_miterateAux___main___at_Lean_IR_Log_format___spec__1___boxed(obj*, obj*, obj*, obj*);
 obj* l_Lean_IR_declMapExt___elambda__1(obj*);
 extern obj* l_Lean_SMap_insert___main___at_Lean_Environment_add___spec__1___closed__2;
+obj* l_Lean_IR_getDecl_x_27(obj*, obj*, obj*, obj*);
 obj* l___private_init_lean_compiler_ir_compilerm_4__mkEntryArray(obj*);
 obj* l_AssocList_replace___main___at___private_init_lean_compiler_ir_compilerm_4__mkEntryArray___spec__7(obj*, obj*, obj*);
 extern obj* l_Lean_Format_sbracket___closed__3;
@@ -126,9 +135,11 @@ namespace lean {
 usize usize_modn(usize, obj*);
 }
 obj* l_HashMapImp_find___at_Lean_IR_findDecl___spec__3___boxed(obj*, obj*);
+obj* l_Lean_IR_getDecl_x_27___boxed(obj*, obj*, obj*, obj*);
 obj* l___private_init_lean_compiler_ir_compilerm_2__logDeclsAux___boxed(obj*, obj*, obj*, obj*, obj*);
 obj* l_mkHashMapImp___rarg(obj*);
 obj* l_Lean_IR_modifyEnv(obj*, obj*, obj*);
+obj* l_Lean_IR_containsDecl_x_27(obj*, obj*, obj*, obj*);
 obj* l_Lean_IR_containsDecl___boxed(obj*, obj*, obj*);
 obj* l___private_init_lean_compiler_ir_compilerm_3__logMessageIfAux___rarg(obj*, obj*, obj*, obj*, obj*);
 uint8 l_HashMapImp_contains___at_Lean_IR_containsDecl___spec__2(obj*, obj*);
@@ -145,6 +156,8 @@ obj* l_Lean_IR_logMessageIf___rarg(obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_IR_declMapExt___elambda__2___boxed(obj*);
 obj* l_AssocList_find___main___at_Lean_IR_findDecl___spec__4___boxed(obj*, obj*);
 obj* l_List_foldl___main___at___private_init_lean_compiler_ir_compilerm_4__mkEntryArray___spec__8___boxed(obj*, obj*, obj*);
+obj* l_Lean_IR_findDecl_x_27___boxed(obj*, obj*, obj*, obj*);
+uint8 l_Array_anyMAux___main___at_Lean_IR_containsDecl_x_27___spec__1(obj*, obj*, obj*);
 obj* l_Lean_IR_addDecl(obj*, obj*, obj*);
 obj* l_Lean_Name_append___main(obj*, obj*);
 namespace lean {
@@ -155,6 +168,7 @@ obj* l_Lean_IR_mkDeclMapExtension___lambda__1(uint8, obj*, obj*);
 obj* l_RBNode_find___main___at_Lean_IR_findDecl___spec__2___boxed(obj*, obj*);
 obj* l_Array_mforAux___main___at_Lean_IR_addDecls___spec__1___boxed(obj*, obj*, obj*, obj*);
 obj* l_List_foldl___main___at___private_init_lean_compiler_ir_compilerm_4__mkEntryArray___spec__8(obj*, obj*, obj*);
+obj* l_Lean_IR_containsDecl_x_27___boxed(obj*, obj*, obj*, obj*);
 obj* l_RBNode_insert___at_Lean_IR_mkDeclMapExtension___spec__4(obj*, obj*, obj*);
 obj* l_Array_miterateAux___main___at_Lean_IR_LogEntry_fmt___main___spec__1(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
 _start:
@@ -2692,31 +2706,33 @@ return x_6;
 obj* _init_l_Lean_IR_mkDeclMapExtension___closed__1() {
 _start:
 {
-obj* x_0; obj* x_1; obj* x_2; obj* x_3; obj* x_4; uint8 x_5; obj* x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_10; uint8 x_11; obj* x_12; obj* x_13; 
+obj* x_0; obj* x_1; obj* x_2; obj* x_3; obj* x_4; uint8 x_5; obj* x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_10; obj* x_11; uint8 x_12; obj* x_13; obj* x_14; 
 x_0 = lean::box(0);
 x_1 = lean::mk_string("IRDecls");
 x_2 = lean_name_mk_string(x_0, x_1);
 x_3 = lean::mk_nat_obj(0ul);
 x_4 = lean::mk_empty_array(x_3);
 x_5 = 6;
-x_6 = lean::alloc_cnstr(1, 2, 1);
-lean::cnstr_set(x_6, 0, x_0);
-lean::cnstr_set(x_6, 1, x_4);
-lean::cnstr_set_scalar(x_6, sizeof(void*)*2, x_5);
-x_7 = x_6;
-x_8 = l_Lean_SMap_empty___at_Lean_IR_mkDeclMapExtension___spec__1;
-x_9 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_IR_mkDeclMapExtension___lambda__1___boxed), 3, 0);
-x_10 = lean::alloc_closure(reinterpret_cast<void*>(l___private_init_lean_compiler_ir_compilerm_4__mkEntryArray), 1, 0);
-x_11 = 0;
-x_12 = lean::alloc_cnstr(0, 5, 1);
-lean::cnstr_set(x_12, 0, x_2);
-lean::cnstr_set(x_12, 1, x_8);
-lean::cnstr_set(x_12, 2, x_7);
-lean::cnstr_set(x_12, 3, x_9);
-lean::cnstr_set(x_12, 4, x_10);
-lean::cnstr_set_scalar(x_12, sizeof(void*)*5, x_11);
-x_13 = x_12;
-return x_13;
+x_6 = lean::box(12);
+x_7 = lean::alloc_cnstr(0, 3, 1);
+lean::cnstr_set(x_7, 0, x_0);
+lean::cnstr_set(x_7, 1, x_4);
+lean::cnstr_set(x_7, 2, x_6);
+lean::cnstr_set_scalar(x_7, sizeof(void*)*3, x_5);
+x_8 = x_7;
+x_9 = l_Lean_SMap_empty___at_Lean_IR_mkDeclMapExtension___spec__1;
+x_10 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_IR_mkDeclMapExtension___lambda__1___boxed), 3, 0);
+x_11 = lean::alloc_closure(reinterpret_cast<void*>(l___private_init_lean_compiler_ir_compilerm_4__mkEntryArray), 1, 0);
+x_12 = 0;
+x_13 = lean::alloc_cnstr(0, 5, 1);
+lean::cnstr_set(x_13, 0, x_2);
+lean::cnstr_set(x_13, 1, x_9);
+lean::cnstr_set(x_13, 2, x_8);
+lean::cnstr_set(x_13, 3, x_10);
+lean::cnstr_set(x_13, 4, x_11);
+lean::cnstr_set_scalar(x_13, sizeof(void*)*5, x_12);
+x_14 = x_13;
+return x_14;
 }
 }
 obj* l_Lean_IR_mkDeclMapExtension(obj* x_0) {
@@ -3250,6 +3266,18 @@ lean::dec(x_1);
 return x_3;
 }
 }
+namespace lean {
+namespace ir {
+obj* add_decl_core(obj* x_0, obj* x_1) {
+_start:
+{
+obj* x_2; obj* x_3; 
+x_2 = l_Lean_IR_declMapExt;
+x_3 = l_Lean_PersistentEnvExtension_addEntry___rarg(x_2, x_0, x_1);
+return x_3;
+}
+}
+}}
 obj* l_Lean_IR_addDecl(obj* x_0, obj* x_1, obj* x_2) {
 _start:
 {
@@ -3419,6 +3447,345 @@ lean::dec(x_1);
 return x_3;
 }
 }
+obj* l_Array_mfindAux___main___at_Lean_IR_findDecl_x_27___spec__1(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; uint8 x_4; 
+x_3 = lean::array_get_size(x_1);
+x_4 = lean::nat_dec_lt(x_2, x_3);
+lean::dec(x_3);
+if (x_4 == 0)
+{
+obj* x_7; 
+lean::dec(x_2);
+x_7 = lean::box(0);
+return x_7;
+}
+else
+{
+obj* x_8; obj* x_9; uint8 x_10; 
+x_8 = lean::array_fget(x_1, x_2);
+x_9 = l_Lean_IR_Decl_name___main(x_8);
+x_10 = lean_name_dec_eq(x_9, x_0);
+lean::dec(x_9);
+if (x_10 == 0)
+{
+obj* x_13; obj* x_14; 
+lean::dec(x_8);
+x_13 = lean::mk_nat_obj(1ul);
+x_14 = lean::nat_add(x_2, x_13);
+lean::dec(x_2);
+x_2 = x_14;
+goto _start;
+}
+else
+{
+obj* x_18; 
+lean::dec(x_2);
+x_18 = lean::alloc_cnstr(1, 1, 0);
+lean::cnstr_set(x_18, 0, x_8);
+return x_18;
+}
+}
+}
+}
+obj* l_Lean_IR_findDecl_x_27(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+obj* x_4; obj* x_5; 
+x_4 = lean::mk_nat_obj(0ul);
+x_5 = l_Array_mfindAux___main___at_Lean_IR_findDecl_x_27___spec__1(x_0, x_1, x_4);
+if (lean::obj_tag(x_5) == 0)
+{
+obj* x_6; obj* x_8; obj* x_9; obj* x_11; obj* x_12; obj* x_14; obj* x_15; 
+x_6 = lean::cnstr_get(x_3, 1);
+if (lean::is_exclusive(x_3)) {
+ lean::cnstr_release(x_3, 0);
+ x_8 = x_3;
+} else {
+ lean::inc(x_6);
+ lean::dec(x_3);
+ x_8 = lean::box(0);
+}
+x_9 = lean::cnstr_get(x_6, 0);
+lean::inc(x_9);
+x_11 = l_Lean_IR_declMapExt;
+x_12 = l_Lean_PersistentEnvExtension_getState___rarg(x_11, x_9);
+lean::dec(x_9);
+x_14 = l_Lean_SMap_find___main___at_Lean_IR_findDecl___spec__1(x_12, x_0);
+if (lean::is_scalar(x_8)) {
+ x_15 = lean::alloc_cnstr(0, 2, 0);
+} else {
+ x_15 = x_8;
+}
+lean::cnstr_set(x_15, 0, x_14);
+lean::cnstr_set(x_15, 1, x_6);
+return x_15;
+}
+else
+{
+obj* x_16; obj* x_18; obj* x_19; 
+x_16 = lean::cnstr_get(x_3, 1);
+if (lean::is_exclusive(x_3)) {
+ lean::cnstr_release(x_3, 0);
+ x_18 = x_3;
+} else {
+ lean::inc(x_16);
+ lean::dec(x_3);
+ x_18 = lean::box(0);
+}
+if (lean::is_scalar(x_18)) {
+ x_19 = lean::alloc_cnstr(0, 2, 0);
+} else {
+ x_19 = x_18;
+}
+lean::cnstr_set(x_19, 0, x_5);
+lean::cnstr_set(x_19, 1, x_16);
+return x_19;
+}
+}
+}
+obj* l_Array_mfindAux___main___at_Lean_IR_findDecl_x_27___spec__1___boxed(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = l_Array_mfindAux___main___at_Lean_IR_findDecl_x_27___spec__1(x_0, x_1, x_2);
+lean::dec(x_0);
+lean::dec(x_1);
+return x_3;
+}
+}
+obj* l_Lean_IR_findDecl_x_27___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+obj* x_4; 
+x_4 = l_Lean_IR_findDecl_x_27(x_0, x_1, x_2, x_3);
+lean::dec(x_0);
+lean::dec(x_1);
+lean::dec(x_2);
+return x_4;
+}
+}
+uint8 l_Array_anyMAux___main___at_Lean_IR_containsDecl_x_27___spec__1(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; uint8 x_4; 
+x_3 = lean::array_get_size(x_1);
+x_4 = lean::nat_dec_lt(x_2, x_3);
+lean::dec(x_3);
+if (x_4 == 0)
+{
+uint8 x_7; 
+lean::dec(x_2);
+x_7 = 0;
+return x_7;
+}
+else
+{
+obj* x_8; obj* x_9; uint8 x_11; 
+x_8 = lean::array_fget(x_1, x_2);
+x_9 = l_Lean_IR_Decl_name___main(x_8);
+lean::dec(x_8);
+x_11 = lean_name_dec_eq(x_9, x_0);
+lean::dec(x_9);
+if (x_11 == 0)
+{
+obj* x_13; obj* x_14; 
+x_13 = lean::mk_nat_obj(1ul);
+x_14 = lean::nat_add(x_2, x_13);
+lean::dec(x_2);
+x_2 = x_14;
+goto _start;
+}
+else
+{
+lean::dec(x_2);
+return x_11;
+}
+}
+}
+}
+obj* l_Lean_IR_containsDecl_x_27(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+obj* x_4; uint8 x_5; 
+x_4 = lean::mk_nat_obj(0ul);
+x_5 = l_Array_anyMAux___main___at_Lean_IR_containsDecl_x_27___spec__1(x_0, x_1, x_4);
+if (x_5 == 0)
+{
+obj* x_6; obj* x_8; obj* x_9; obj* x_11; obj* x_12; uint8 x_14; obj* x_15; obj* x_16; 
+x_6 = lean::cnstr_get(x_3, 1);
+if (lean::is_exclusive(x_3)) {
+ lean::cnstr_release(x_3, 0);
+ x_8 = x_3;
+} else {
+ lean::inc(x_6);
+ lean::dec(x_3);
+ x_8 = lean::box(0);
+}
+x_9 = lean::cnstr_get(x_6, 0);
+lean::inc(x_9);
+x_11 = l_Lean_IR_declMapExt;
+x_12 = l_Lean_PersistentEnvExtension_getState___rarg(x_11, x_9);
+lean::dec(x_9);
+x_14 = l_Lean_SMap_contains___main___at_Lean_IR_containsDecl___spec__1(x_12, x_0);
+x_15 = lean::box(x_14);
+if (lean::is_scalar(x_8)) {
+ x_16 = lean::alloc_cnstr(0, 2, 0);
+} else {
+ x_16 = x_8;
+}
+lean::cnstr_set(x_16, 0, x_15);
+lean::cnstr_set(x_16, 1, x_6);
+return x_16;
+}
+else
+{
+obj* x_17; obj* x_19; uint8 x_20; obj* x_21; obj* x_22; 
+x_17 = lean::cnstr_get(x_3, 1);
+if (lean::is_exclusive(x_3)) {
+ lean::cnstr_release(x_3, 0);
+ x_19 = x_3;
+} else {
+ lean::inc(x_17);
+ lean::dec(x_3);
+ x_19 = lean::box(0);
+}
+x_20 = 1;
+x_21 = lean::box(x_20);
+if (lean::is_scalar(x_19)) {
+ x_22 = lean::alloc_cnstr(0, 2, 0);
+} else {
+ x_22 = x_19;
+}
+lean::cnstr_set(x_22, 0, x_21);
+lean::cnstr_set(x_22, 1, x_17);
+return x_22;
+}
+}
+}
+obj* l_Array_anyMAux___main___at_Lean_IR_containsDecl_x_27___spec__1___boxed(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+uint8 x_3; obj* x_4; 
+x_3 = l_Array_anyMAux___main___at_Lean_IR_containsDecl_x_27___spec__1(x_0, x_1, x_2);
+x_4 = lean::box(x_3);
+lean::dec(x_0);
+lean::dec(x_1);
+return x_4;
+}
+}
+obj* l_Lean_IR_containsDecl_x_27___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+obj* x_4; 
+x_4 = l_Lean_IR_containsDecl_x_27(x_0, x_1, x_2, x_3);
+lean::dec(x_0);
+lean::dec(x_1);
+lean::dec(x_2);
+return x_4;
+}
+}
+obj* l_Lean_IR_getDecl_x_27(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+obj* x_4; 
+x_4 = l_Lean_IR_findDecl_x_27(x_0, x_1, x_2, x_3);
+if (lean::obj_tag(x_4) == 0)
+{
+obj* x_5; 
+x_5 = lean::cnstr_get(x_4, 0);
+lean::inc(x_5);
+if (lean::obj_tag(x_5) == 0)
+{
+obj* x_7; obj* x_9; obj* x_10; obj* x_11; obj* x_12; obj* x_13; obj* x_15; obj* x_16; obj* x_17; 
+x_7 = lean::cnstr_get(x_4, 1);
+if (lean::is_exclusive(x_4)) {
+ lean::cnstr_release(x_4, 0);
+ x_9 = x_4;
+} else {
+ lean::inc(x_7);
+ lean::dec(x_4);
+ x_9 = lean::box(0);
+}
+x_10 = l_Lean_Name_toString___closed__1;
+x_11 = l_Lean_Name_toStringWithSep___main(x_10, x_0);
+x_12 = l_Lean_IR_getDecl___closed__1;
+x_13 = lean::string_append(x_12, x_11);
+lean::dec(x_11);
+x_15 = l_Char_HasRepr___closed__1;
+x_16 = lean::string_append(x_13, x_15);
+if (lean::is_scalar(x_9)) {
+ x_17 = lean::alloc_cnstr(1, 2, 0);
+} else {
+ x_17 = x_9;
+ lean::cnstr_set_tag(x_9, 1);
+}
+lean::cnstr_set(x_17, 0, x_16);
+lean::cnstr_set(x_17, 1, x_7);
+return x_17;
+}
+else
+{
+obj* x_19; obj* x_21; obj* x_22; obj* x_25; 
+lean::dec(x_0);
+x_19 = lean::cnstr_get(x_4, 1);
+if (lean::is_exclusive(x_4)) {
+ lean::cnstr_release(x_4, 0);
+ x_21 = x_4;
+} else {
+ lean::inc(x_19);
+ lean::dec(x_4);
+ x_21 = lean::box(0);
+}
+x_22 = lean::cnstr_get(x_5, 0);
+lean::inc(x_22);
+lean::dec(x_5);
+if (lean::is_scalar(x_21)) {
+ x_25 = lean::alloc_cnstr(0, 2, 0);
+} else {
+ x_25 = x_21;
+}
+lean::cnstr_set(x_25, 0, x_22);
+lean::cnstr_set(x_25, 1, x_19);
+return x_25;
+}
+}
+else
+{
+obj* x_27; obj* x_29; obj* x_31; obj* x_32; 
+lean::dec(x_0);
+x_27 = lean::cnstr_get(x_4, 0);
+x_29 = lean::cnstr_get(x_4, 1);
+if (lean::is_exclusive(x_4)) {
+ x_31 = x_4;
+} else {
+ lean::inc(x_27);
+ lean::inc(x_29);
+ lean::dec(x_4);
+ x_31 = lean::box(0);
+}
+if (lean::is_scalar(x_31)) {
+ x_32 = lean::alloc_cnstr(1, 2, 0);
+} else {
+ x_32 = x_31;
+}
+lean::cnstr_set(x_32, 0, x_27);
+lean::cnstr_set(x_32, 1, x_29);
+return x_32;
+}
+}
+}
+obj* l_Lean_IR_getDecl_x_27___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+obj* x_4; 
+x_4 = l_Lean_IR_getDecl_x_27(x_0, x_1, x_2, x_3);
+lean::dec(x_1);
+lean::dec(x_2);
+return x_4;
+}
+}
 obj* initialize_init_control_reader(obj*);
 obj* initialize_init_lean_environment(obj*);
 obj* initialize_init_lean_compiler_ir_basic(obj*);
diff --git a/src/stage0/init/lean/compiler/ir/default.cpp b/src/stage0/init/lean/compiler/ir/default.cpp
index ddf1ca1e98..be2525221d 100644
--- a/src/stage0/init/lean/compiler/ir/default.cpp
+++ b/src/stage0/init/lean/compiler/ir/default.cpp
@@ -56,17 +56,19 @@ obj* l_Array_hmmapAux___main___at___private_init_lean_compiler_ir_default_1__com
 obj* _init_l_Array_hmmapAux___main___at___private_init_lean_compiler_ir_default_1__compileAux___spec__1___closed__1() {
 _start:
 {
-obj* x_0; obj* x_1; obj* x_2; uint8 x_3; obj* x_4; obj* x_5; 
+obj* x_0; obj* x_1; obj* x_2; uint8 x_3; obj* x_4; obj* x_5; obj* x_6; 
 x_0 = lean::mk_nat_obj(0ul);
 x_1 = lean::mk_empty_array(x_0);
 x_2 = lean::box(0);
 x_3 = 6;
-x_4 = lean::alloc_cnstr(1, 2, 1);
-lean::cnstr_set(x_4, 0, x_2);
-lean::cnstr_set(x_4, 1, x_1);
-lean::cnstr_set_scalar(x_4, sizeof(void*)*2, x_3);
-x_5 = x_4;
-return x_5;
+x_4 = lean::box(12);
+x_5 = lean::alloc_cnstr(0, 3, 1);
+lean::cnstr_set(x_5, 0, x_2);
+lean::cnstr_set(x_5, 1, x_1);
+lean::cnstr_set(x_5, 2, x_4);
+lean::cnstr_set_scalar(x_5, sizeof(void*)*3, x_3);
+x_6 = x_5;
+return x_6;
 }
 }
 obj* l_Array_hmmapAux___main___at___private_init_lean_compiler_ir_default_1__compileAux___spec__1(obj* x_0, obj* x_1) {
diff --git a/src/stage0/init/lean/compiler/ir/format.cpp b/src/stage0/init/lean/compiler/ir/format.cpp
index 730791b912..75e4304fdd 100644
--- a/src/stage0/init/lean/compiler/ir/format.cpp
+++ b/src/stage0/init/lean/compiler/ir/format.cpp
@@ -2832,7 +2832,7 @@ x_41 = lean::cnstr_get(x_1, 0);
 lean::inc(x_41);
 x_43 = lean::cnstr_get(x_1, 1);
 lean::inc(x_43);
-x_45 = lean::cnstr_get_scalar<uint8>(x_1, sizeof(void*)*2);
+x_45 = lean::cnstr_get_scalar<uint8>(x_1, sizeof(void*)*3);
 lean::dec(x_1);
 x_47 = l_Lean_Name_toString___closed__1;
 x_48 = l_Lean_Name_toStringWithSep___main(x_47, x_41);