diff --git a/library/init/lean/level.lean b/library/init/lean/level.lean
index 034394772d..1dc6bcf55f 100644
--- a/library/init/lean/level.lean
+++ b/library/init/lean/level.lean
@@ -16,6 +16,12 @@ inductive level
 | param  : name → level
 | mvar   : name → level
 
+attribute [extern "level_mk_succ"]  level.succ
+attribute [extern "level_mk_max"]   level.max
+attribute [extern "level_mk_imax"]  level.imax
+attribute [extern "level_mk_param"] level.param
+attribute [extern "level_mk_mvar"]  level.mvar
+
 instance level_is_inhabited : inhabited level :=
 ⟨level.zero⟩
 
diff --git a/src/boot/init/lean/elaborator.cpp b/src/boot/init/lean/elaborator.cpp
index ee7ea3f97e..c44de5a3aa 100644
--- a/src/boot/init/lean/elaborator.cpp
+++ b/src/boot/init/lean/elaborator.cpp
@@ -259,6 +259,7 @@ obj* l_lean_parser_syntax_get__pos(obj*);
 obj* l_list_foldl___main___at_lean_elaborator_elaborators___spec__5(obj*, obj*);
 obj* l_lean_elaborator_mk__notation__kind(obj*);
 obj* l_lean_elaborator_locally___at_lean_elaborator_declaration_elaborate___spec__14___closed__7;
+extern "C" obj* level_mk_imax(obj*, obj*);
 obj* l_lean_environment_mk__empty___boxed(obj*);
 obj* l_lean_elaborator_attribute_elaborate___closed__2;
 obj* l_lean_elaborator_locally___at_lean_elaborator_declaration_elaborate___spec__14___closed__6;
@@ -338,6 +339,7 @@ extern obj* l_lean_parser_command_attribute;
 extern obj* l_lean_parser_term_let_has__view;
 obj* l_list_mmap___main___at_lean_elaborator_command__parser__config_register__notation__parser___spec__2___closed__3;
 obj* l_lean_elaborator_elaborator__m__coe__coelaborator__m___rarg(obj*, obj*, obj*, obj*);
+extern "C" obj* level_mk_succ(obj*);
 obj* l_list_foldr___main___at_lean_elaborator_to__level___main___spec__2(obj*, obj*);
 obj* l_list_foldr___main___at_lean_elaborator_to__pexpr___main___spec__15(obj*);
 obj* l_lean_elaborator_to__pexpr___main___closed__14;
@@ -479,6 +481,7 @@ extern obj* l_lean_parser_command_section;
 obj* l_list_mfilter___main___at_lean_elaborator_variables_elaborate___spec__4(obj*, obj*, obj*);
 obj* l_reader__t_lift(obj*, obj*, obj*, obj*);
 obj* l_lean_elaborator_to__pexpr___main___closed__21;
+extern "C" obj* level_mk_max(obj*, obj*);
 obj* l_lean_elaborator_locally___at_lean_elaborator_section_elaborate___spec__2___lambda__4(obj*, obj*, obj*, obj*);
 extern obj* l_lean_parser_term_struct__inst__item_has__view;
 obj* l_lean_elaborator_yield__to__outside___rarg___lambda__2(obj*);
@@ -550,6 +553,7 @@ obj* l_lean_elaborator_level__add___main(obj*, obj*);
 obj* l_lean_elaborator_elaborate__command___boxed(obj*, obj*, obj*);
 obj* l_reader__t_monad___rarg(obj*);
 obj* l_lean_expr_mk__capp(obj*, obj*);
+extern "C" obj* level_mk_mvar(obj*);
 obj* l_list_foldr___main___at_lean_elaborator_to__level___main___spec__4(obj*, obj*);
 obj* l_lean_elaborator_commands_elaborate___main___lambda__2(uint8, obj*, obj*, obj*, obj*);
 obj* l_lean_elaborator_to__pexpr___main(obj*, obj*, obj*);
@@ -608,6 +612,7 @@ obj* l_lean_elaborator_old__elab__command(obj*, obj*, obj*, obj*);
 obj* l_list_map___main___at_lean_elaborator_declaration_elaborate___spec__13(obj*);
 obj* l_option_to__monad___main___at_lean_elaborator_command__parser__config_register__notation__parser___spec__1(obj*);
 obj* l_lean_file__map_to__position(obj*, obj*);
+extern "C" obj* level_mk_param(obj*);
 obj* l_lean_name_quick__lt___main(obj*, obj*);
 obj* l_state__t_lift___rarg(obj*, obj*, obj*, obj*);
 extern "C" obj* lean_elaborator_elaborate_command(obj*, obj*, obj*);
@@ -2335,8 +2340,7 @@ x_6 = lean::nat_sub(x_1, x_5);
 lean::dec(x_5);
 lean::dec(x_1);
 x_9 = l_lean_elaborator_level__add___main(x_0, x_6);
-x_10 = lean::alloc_cnstr(1, 1, 0);
-lean::cnstr_set(x_10, 0, x_9);
+x_10 = level_mk_succ(x_9);
 return x_10;
 }
 else
@@ -2507,9 +2511,7 @@ x_5 = lean::cnstr_get(x_1, 1);
 lean::inc(x_5);
 lean::dec(x_1);
 x_8 = l_list_foldr___main___at_lean_elaborator_to__level___main___spec__2(x_0, x_5);
-x_9 = lean::alloc_cnstr(2, 2, 0);
-lean::cnstr_set(x_9, 0, x_3);
-lean::cnstr_set(x_9, 1, x_8);
+x_9 = level_mk_max(x_3, x_8);
 return x_9;
 }
 }
@@ -2667,9 +2669,7 @@ x_5 = lean::cnstr_get(x_1, 1);
 lean::inc(x_5);
 lean::dec(x_1);
 x_8 = l_list_foldr___main___at_lean_elaborator_to__level___main___spec__4(x_0, x_5);
-x_9 = lean::alloc_cnstr(3, 2, 0);
-lean::cnstr_set(x_9, 0, x_3);
-lean::cnstr_set(x_9, 1, x_8);
+x_9 = level_mk_imax(x_3, x_8);
 return x_9;
 }
 }
@@ -2714,8 +2714,7 @@ _start:
 {
 obj* x_0; obj* x_1; 
 x_0 = lean::box(0);
-x_1 = lean::alloc_cnstr(5, 1, 0);
-lean::cnstr_set(x_1, 0, x_0);
+x_1 = level_mk_mvar(x_0);
 return x_1;
 }
 }
@@ -3282,8 +3281,7 @@ obj* x_276; obj* x_277; obj* x_278;
 lean::dec(x_259);
 lean::dec(x_1);
 lean::dec(x_0);
-x_276 = lean::alloc_cnstr(4, 1, 0);
-lean::cnstr_set(x_276, 0, x_252);
+x_276 = level_mk_param(x_252);
 if (lean::is_scalar(x_19)) {
  x_277 = lean::alloc_cnstr(0, 2, 0);
 } else {
@@ -7929,8 +7927,7 @@ _start:
 {
 obj* x_0; obj* x_1; obj* x_2; 
 x_0 = lean::box(0);
-x_1 = lean::alloc_cnstr(1, 1, 0);
-lean::cnstr_set(x_1, 0, x_0);
+x_1 = level_mk_succ(x_0);
 x_2 = lean::alloc_cnstr(3, 1, 0);
 lean::cnstr_set(x_2, 0, x_1);
 return x_2;
@@ -11148,8 +11145,7 @@ if (lean::is_shared(x_1573)) {
  lean::cnstr_release(x_1573, 1);
  x_1580 = x_1573;
 }
-x_1581 = lean::alloc_cnstr(1, 1, 0);
-lean::cnstr_set(x_1581, 0, x_1576);
+x_1581 = level_mk_succ(x_1576);
 x_1582 = lean::alloc_cnstr(3, 1, 0);
 lean::cnstr_set(x_1582, 0, x_1581);
 if (lean::is_scalar(x_1580)) {
@@ -14499,8 +14495,7 @@ if (lean::is_shared(x_0)) {
  x_7 = x_0;
 }
 x_8 = l_lean_elaborator_mangle__ident(x_3);
-x_9 = lean::alloc_cnstr(4, 1, 0);
-lean::cnstr_set(x_9, 0, x_8);
+x_9 = level_mk_param(x_8);
 x_10 = l_list_map___main___at_lean_elaborator_ident__univ__params__to__pexpr___spec__1(x_5);
 if (lean::is_scalar(x_7)) {
  x_11 = lean::alloc_cnstr(1, 2, 0);
@@ -15374,8 +15369,7 @@ x_5 = lean::cnstr_get(x_1, 1);
 lean::inc(x_5);
 lean::dec(x_1);
 lean::inc(x_3);
-x_9 = lean::alloc_cnstr(4, 1, 0);
-lean::cnstr_set(x_9, 0, x_3);
+x_9 = level_mk_param(x_3);
 x_10 = l_lean_elaborator_ordered__rbmap_insert___at_lean_elaborator_elab__def__like___spec__4(x_0, x_3, x_9);
 x_0 = x_10;
 x_1 = x_5;
@@ -16597,8 +16591,7 @@ x_5 = lean::cnstr_get(x_1, 1);
 lean::inc(x_5);
 lean::dec(x_1);
 lean::inc(x_3);
-x_9 = lean::alloc_cnstr(4, 1, 0);
-lean::cnstr_set(x_9, 0, x_3);
+x_9 = level_mk_param(x_3);
 x_10 = l_lean_elaborator_ordered__rbmap_insert___at_lean_elaborator_elab__def__like___spec__4(x_0, x_3, x_9);
 x_0 = x_10;
 x_1 = x_5;
@@ -17240,8 +17233,7 @@ x_5 = lean::cnstr_get(x_1, 1);
 lean::inc(x_5);
 lean::dec(x_1);
 lean::inc(x_3);
-x_9 = lean::alloc_cnstr(4, 1, 0);
-lean::cnstr_set(x_9, 0, x_3);
+x_9 = level_mk_param(x_3);
 x_10 = l_lean_elaborator_ordered__rbmap_insert___at_lean_elaborator_elab__def__like___spec__4(x_0, x_3, x_9);
 x_0 = x_10;
 x_1 = x_5;
@@ -23551,8 +23543,7 @@ lean::inc(x_28);
 x_30 = lean::cnstr_get(x_12, 0);
 lean::inc(x_30);
 lean::inc(x_11);
-x_33 = lean::alloc_cnstr(4, 1, 0);
-lean::cnstr_set(x_33, 0, x_11);
+x_33 = level_mk_param(x_11);
 x_34 = l_lean_elaborator_ordered__rbmap_insert___at_lean_elaborator_elab__def__like___spec__4(x_14, x_11, x_33);
 x_35 = lean::cnstr_get(x_12, 2);
 lean::inc(x_35);
diff --git a/src/boot/init/lean/level.cpp b/src/boot/init/lean/level.cpp
index b1e213bc20..f0096113e1 100644
--- a/src/boot/init/lean/level.cpp
+++ b/src/boot/init/lean/level.cpp
@@ -41,6 +41,7 @@ obj* l_lean_level__to__format_result_to__format___main___boxed(obj*, obj*);
 extern obj* l_lean_name_to__string___closed__1;
 obj* l_function_comp___rarg(obj*, obj*, obj*);
 obj* l_lean_level__to__format_result_imax___main(obj*, obj*);
+extern "C" obj* level_mk_imax(obj*, obj*);
 obj* l_lean_name_to__string__with__sep___main(obj*, obj*);
 obj* l_lean_level__to__format_paren__if__false___main(obj*, uint8);
 obj* l_lean_level__to__format_result_max(obj*, obj*);
@@ -54,6 +55,7 @@ obj* l_lean_level_to__offset(obj*);
 obj* l_lean_level__to__format_result_to__format___main___closed__1;
 obj* l_lean_level_of__nat(obj*);
 obj* l_lean_level_has__param___main(obj*);
+extern "C" obj* level_mk_succ(obj*);
 obj* l_lean_level__to__format_level_to__result___main___closed__1;
 obj* l_lean_level_to__nat___main___closed__2;
 obj* l_lean_level__to__format_result_to__format___boxed(obj*, obj*);
@@ -64,6 +66,7 @@ extern obj* l_lean_format_paren___closed__3;
 obj* l_lean_level_to__nat___main___lambda__1(obj*);
 obj* l_lean_level__to__format_result_max___main(obj*, obj*);
 obj* l_lean_level__to__format_level_to__result(obj*);
+extern "C" obj* level_mk_max(obj*, obj*);
 obj* l_lean_to__fmt___at_lean_level__to__format_result_to__format___main___spec__1(obj*);
 obj* l_lean_level_of__nat___main(obj*);
 extern obj* l_lean_format_paren___closed__2;
@@ -289,8 +292,7 @@ x_5 = lean::nat_sub(x_0, x_4);
 lean::dec(x_4);
 lean::dec(x_0);
 x_8 = l_lean_level_of__nat___main(x_5);
-x_9 = lean::alloc_cnstr(1, 1, 0);
-lean::cnstr_set(x_9, 0, x_8);
+x_9 = level_mk_succ(x_8);
 return x_9;
 }
 else
@@ -592,77 +594,40 @@ return x_1;
 }
 case 1:
 {
-obj* x_3; obj* x_5; obj* x_6; obj* x_7; 
+obj* x_3; obj* x_6; obj* x_7; 
 x_3 = lean::cnstr_get(x_1, 0);
 lean::inc(x_3);
-if (lean::is_shared(x_1)) {
- lean::dec(x_1);
- x_5 = lean::box(0);
-} else {
- lean::cnstr_release(x_1, 0);
- x_5 = x_1;
-}
+lean::dec(x_1);
 x_6 = l_lean_level_instantiate___main(x_0, x_3);
-if (lean::is_scalar(x_5)) {
- x_7 = lean::alloc_cnstr(1, 1, 0);
-} else {
- x_7 = x_5;
-}
-lean::cnstr_set(x_7, 0, x_6);
+x_7 = level_mk_succ(x_6);
 return x_7;
 }
 case 2:
 {
-obj* x_8; obj* x_10; obj* x_12; obj* x_14; obj* x_15; obj* x_16; 
+obj* x_8; obj* x_10; obj* x_14; obj* x_15; obj* x_16; 
 x_8 = lean::cnstr_get(x_1, 0);
 lean::inc(x_8);
 x_10 = lean::cnstr_get(x_1, 1);
 lean::inc(x_10);
-if (lean::is_shared(x_1)) {
- lean::dec(x_1);
- x_12 = lean::box(0);
-} else {
- lean::cnstr_release(x_1, 0);
- lean::cnstr_release(x_1, 1);
- x_12 = x_1;
-}
+lean::dec(x_1);
 lean::inc(x_0);
 x_14 = l_lean_level_instantiate___main(x_0, x_8);
 x_15 = l_lean_level_instantiate___main(x_0, x_10);
-if (lean::is_scalar(x_12)) {
- x_16 = lean::alloc_cnstr(2, 2, 0);
-} else {
- x_16 = x_12;
-}
-lean::cnstr_set(x_16, 0, x_14);
-lean::cnstr_set(x_16, 1, x_15);
+x_16 = level_mk_max(x_14, x_15);
 return x_16;
 }
 case 3:
 {
-obj* x_17; obj* x_19; obj* x_21; obj* x_23; obj* x_24; obj* x_25; 
+obj* x_17; obj* x_19; obj* x_23; obj* x_24; obj* x_25; 
 x_17 = lean::cnstr_get(x_1, 0);
 lean::inc(x_17);
 x_19 = lean::cnstr_get(x_1, 1);
 lean::inc(x_19);
-if (lean::is_shared(x_1)) {
- lean::dec(x_1);
- x_21 = lean::box(0);
-} else {
- lean::cnstr_release(x_1, 0);
- lean::cnstr_release(x_1, 1);
- x_21 = x_1;
-}
+lean::dec(x_1);
 lean::inc(x_0);
 x_23 = l_lean_level_instantiate___main(x_0, x_17);
 x_24 = l_lean_level_instantiate___main(x_0, x_19);
-if (lean::is_scalar(x_21)) {
- x_25 = lean::alloc_cnstr(3, 2, 0);
-} else {
- x_25 = x_21;
-}
-lean::cnstr_set(x_25, 0, x_23);
-lean::cnstr_set(x_25, 1, x_24);
+x_25 = level_mk_imax(x_23, x_24);
 return x_25;
 }
 case 4:
diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp
index 3ea052883b..fc069a35e9 100644
--- a/src/kernel/level.cpp
+++ b/src/kernel/level.cpp
@@ -89,7 +89,7 @@ bool level_has_mvar(b_obj_arg l) {
     lean_unreachable(); // LCOV_EXCL_LINE
 }
 
-object * level_mk_succ(obj_arg l) {
+extern "C" object * level_mk_succ(obj_arg l) {
     object * r = alloc_cnstr(static_cast<unsigned>(level_kind::Succ), 1, g_level_num_scalars);
     cnstr_set(r, 0, l);
     set_level_scalar_fields(r, 1, hash(level_hash(l), 17u), level_depth(l)+1, level_has_param(l), level_has_mvar(l));
@@ -108,21 +108,21 @@ template<level_kind k> object * level_mk_max_imax(obj_arg l1, obj_arg l2) {
     return r;
 }
 
-object * level_mk_max(obj_arg l1, obj_arg l2) {
+extern "C" object * level_mk_max(obj_arg l1, obj_arg l2) {
     return level_mk_max_imax<level_kind::Max>(l1, l2);
 }
 
-object * level_mk_imax(obj_arg l1, obj_arg l2) {
+extern "C" object * level_mk_imax(obj_arg l1, obj_arg l2) {
     return level_mk_max_imax<level_kind::IMax>(l1, l2);
 }
 
-object * level_mk_univ_param(obj_arg n) {
+extern "C" object * level_mk_param(obj_arg n) {
     object * r = alloc_cnstr(static_cast<unsigned>(level_kind::Param), 1, 0);
     cnstr_set(r, 0, n);
     return r;
 }
 
-object * level_mk_univ_mvar(obj_arg n) {
+extern "C" object * level_mk_mvar(obj_arg n) {
     object * r = alloc_cnstr(static_cast<unsigned>(level_kind::MVar), 1, 0);
     cnstr_set(r, 0, n);
     return r;
@@ -145,12 +145,12 @@ level mk_imax_core(level const & l1, level const & l2) {
 
 level mk_univ_param(name const & n) {
     inc(n.raw());
-    return level(level_mk_univ_param(n.raw()));
+    return level(level_mk_param(n.raw()));
 }
 
 level mk_univ_mvar(name const & n) {
     inc(n.raw());
-    return level(level_mk_univ_mvar(n.raw()));
+    return level(level_mk_mvar(n.raw()));
 }
 
 unsigned level::hash() const { return level_hash(raw()); }