diff --git a/library/init/data/basic.lean b/library/init/data/basic.lean
index cd9e8d9974..0475dd864c 100644
--- a/library/init/data/basic.lean
+++ b/library/init/data/basic.lean
@@ -6,5 +6,5 @@ Authors: Leonardo de Moura
 prelude
 import init.data.nat.basic init.data.fin.basic init.data.list.basic init.data.char.basic
 import init.data.string.basic init.data.option.basic
-import init.data.uint init.data.ordering.basic init.data.repr
+import init.data.uint init.data.repr
 import init.data.tostring
diff --git a/library/init/data/default.lean b/library/init/data/default.lean
index 0be0f172bc..41ca75b3d0 100644
--- a/library/init/data/default.lean
+++ b/library/init/data/default.lean
@@ -6,6 +6,6 @@ Authors: Leonardo de Moura
 prelude
 import init.data.basic init.data.nat init.data.char init.data.string
 import init.data.list init.data.int init.data.array init.data.bytearray
-import init.data.fin init.data.uint init.data.ordering
+import init.data.fin init.data.uint
 import init.data.rbtree init.data.rbmap init.data.option.basic init.data.option.instances
 import init.data.hashmap init.data.random
diff --git a/library/init/data/ordering/basic.lean b/library/init/data/ordering/basic.lean
deleted file mode 100644
index c3c2bccea6..0000000000
--- a/library/init/data/ordering/basic.lean
+++ /dev/null
@@ -1,59 +0,0 @@
-/-
-Copyright (c) 2016 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import init.data.repr
-
-universes u v
-
-inductive Ordering
-| lt | Eq | gt
-
-instance : HasRepr Ordering :=
-⟨(fun s => match s with | Ordering.lt => "lt" | Ordering.Eq => "Eq" | Ordering.gt => "gt")⟩
-
-namespace Ordering
-def swap : Ordering → Ordering
-| lt => gt
-| Eq => Eq
-| gt => lt
-
-@[inline] def orElse : Ordering → Ordering → Ordering
-| lt, _ => lt
-| Eq, o => o
-| gt, _ => gt
-
-theorem swapSwap : ∀ (o : Ordering), o.swap.swap = o
-| lt => rfl
-| Eq => rfl
-| gt => rfl
-end Ordering
-
-@[inline] def cmpUsing {α : Type u} (lt : α → α → Prop) [DecidableRel lt] (a b : α) : Ordering :=
-if lt a b      then Ordering.lt
-else if lt b a then Ordering.gt
-else                Ordering.Eq
-
-def cmp {α : Type u} [HasLess α] [DecidableRel (HasLess.Less : α → α → Prop)] (a b : α) : Ordering :=
-cmpUsing HasLess.Less a b
-
-instance : DecidableEq Ordering :=
-{decEq := fun a b =>
-  match a with
-  | Ordering.lt =>
-    match b with
-    | Ordering.lt => isTrue rfl
-    | Ordering.Eq => isFalse (fun h => Ordering.noConfusion h)
-    | Ordering.gt => isFalse (fun h => Ordering.noConfusion h)
-  | Ordering.Eq =>
-    match b with
-    | Ordering.lt => isFalse (fun h => Ordering.noConfusion h)
-    | Ordering.Eq => isTrue rfl
-    | Ordering.gt => isFalse (fun h => Ordering.noConfusion h)
-  | Ordering.gt =>
-    match b with
-    | Ordering.lt => isFalse (fun h => Ordering.noConfusion h)
-    | Ordering.Eq => isFalse (fun h => Ordering.noConfusion h)
-    | Ordering.gt => isTrue rfl}
diff --git a/library/init/data/ordering/default.lean b/library/init/data/ordering/default.lean
deleted file mode 100644
index e3f5fdf672..0000000000
--- a/library/init/data/ordering/default.lean
+++ /dev/null
@@ -1,7 +0,0 @@
-/-
-Copyright (c) 2017 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import .basic
diff --git a/src/stage0/CMakeLists.txt b/src/stage0/CMakeLists.txt
index ec7a1d475b..de96aa09b9 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/binomialheap/basic.cpp ./init/data/binomialheap/default.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/persistenthashmap/basic.cpp ./init/data/persistenthashmap/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/fix.cpp ./init/lean/attributes.cpp ./init/lean/class.cpp ./init/lean/compiler/closedtermcache.cpp ./init/lean/compiler/constfolding.cpp ./init/lean/compiler/default.cpp ./init/lean/compiler/exportattr.cpp ./init/lean/compiler/externattr.cpp ./init/lean/compiler/implementedbyattr.cpp ./init/lean/compiler/initattr.cpp ./init/lean/compiler/inlineattrs.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/namemangling.cpp ./init/lean/compiler/specialize.cpp ./init/lean/compiler/util.cpp ./init/lean/declaration.cpp ./init/lean/default.cpp ./init/lean/elaborator/alias.cpp ./init/lean/elaborator/basic.cpp ./init/lean/elaborator/command.cpp ./init/lean/elaborator/default.cpp ./init/lean/elaborator/elabstrategyattrs.cpp ./init/lean/environment.cpp ./init/lean/eqncompiler/default.cpp ./init/lean/eqncompiler/matchpattern.cpp ./init/lean/expr.cpp ./init/lean/format.cpp ./init/lean/kvmap.cpp ./init/lean/level.cpp ./init/lean/localcontext.cpp ./init/lean/message.cpp ./init/lean/metavarcontext.cpp ./init/lean/modifiers.cpp ./init/lean/name.cpp ./init/lean/namegenerator.cpp ./init/lean/options.cpp ./init/lean/parser/command.cpp ./init/lean/parser/default.cpp ./init/lean/parser/identifier.cpp ./init/lean/parser/level.cpp ./init/lean/parser/module.cpp ./init/lean/parser/parser.cpp ./init/lean/parser/term.cpp ./init/lean/parser/transform.cpp ./init/lean/parser/trie.cpp ./init/lean/path.cpp ./init/lean/position.cpp ./init/lean/projfns.cpp ./init/lean/reducibilityattrs.cpp ./init/lean/runtime.cpp ./init/lean/scopes.cpp ./init/lean/smap.cpp ./init/lean/syntax.cpp ./init/lean/toexpr.cpp ./init/lean/trace.cpp ./init/lean/util.cpp ./init/system/default.cpp ./init/system/filepath.cpp ./init/system/io.cpp ./init/system/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/binomialheap/basic.cpp ./init/data/binomialheap/default.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/persistentarray/basic.cpp ./init/data/persistentarray/default.cpp ./init/data/persistenthashmap/basic.cpp ./init/data/persistenthashmap/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/fix.cpp ./init/lean/attributes.cpp ./init/lean/class.cpp ./init/lean/compiler/closedtermcache.cpp ./init/lean/compiler/constfolding.cpp ./init/lean/compiler/default.cpp ./init/lean/compiler/exportattr.cpp ./init/lean/compiler/externattr.cpp ./init/lean/compiler/implementedbyattr.cpp ./init/lean/compiler/initattr.cpp ./init/lean/compiler/inlineattrs.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/namemangling.cpp ./init/lean/compiler/specialize.cpp ./init/lean/compiler/util.cpp ./init/lean/declaration.cpp ./init/lean/default.cpp ./init/lean/elaborator/alias.cpp ./init/lean/elaborator/basic.cpp ./init/lean/elaborator/command.cpp ./init/lean/elaborator/default.cpp ./init/lean/elaborator/elabstrategyattrs.cpp ./init/lean/environment.cpp ./init/lean/eqncompiler/default.cpp ./init/lean/eqncompiler/matchpattern.cpp ./init/lean/expr.cpp ./init/lean/format.cpp ./init/lean/kvmap.cpp ./init/lean/level.cpp ./init/lean/localcontext.cpp ./init/lean/message.cpp ./init/lean/metavarcontext.cpp ./init/lean/modifiers.cpp ./init/lean/name.cpp ./init/lean/namegenerator.cpp ./init/lean/options.cpp ./init/lean/parser/command.cpp ./init/lean/parser/default.cpp ./init/lean/parser/identifier.cpp ./init/lean/parser/level.cpp ./init/lean/parser/module.cpp ./init/lean/parser/parser.cpp ./init/lean/parser/term.cpp ./init/lean/parser/transform.cpp ./init/lean/parser/trie.cpp ./init/lean/path.cpp ./init/lean/position.cpp ./init/lean/projfns.cpp ./init/lean/reducibilityattrs.cpp ./init/lean/runtime.cpp ./init/lean/scopes.cpp ./init/lean/smap.cpp ./init/lean/syntax.cpp ./init/lean/toexpr.cpp ./init/lean/trace.cpp ./init/lean/util.cpp ./init/system/default.cpp ./init/system/filepath.cpp ./init/system/io.cpp ./init/system/platform.cpp ./init/util.cpp ./init/wf.cpp)
diff --git a/src/stage0/init/data/basic.cpp b/src/stage0/init/data/basic.cpp
index e42295ed64..a84e69647a 100644
--- a/src/stage0/init/data/basic.cpp
+++ b/src/stage0/init/data/basic.cpp
@@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: init.data.basic
-// Imports: init.data.nat.basic init.data.fin.basic init.data.list.basic init.data.char.basic init.data.string.basic init.data.option.basic init.data.uint init.data.ordering.basic init.data.repr init.data.tostring
+// Imports: init.data.nat.basic init.data.fin.basic init.data.list.basic init.data.char.basic init.data.string.basic init.data.option.basic init.data.uint init.data.repr init.data.tostring
 #include "runtime/object.h"
 #include "runtime/apply.h"
 typedef lean::object obj;    typedef lean::usize  usize;
@@ -21,7 +21,6 @@ obj* initialize_init_data_char_basic(obj*);
 obj* initialize_init_data_string_basic(obj*);
 obj* initialize_init_data_option_basic(obj*);
 obj* initialize_init_data_uint(obj*);
-obj* initialize_init_data_ordering_basic(obj*);
 obj* initialize_init_data_repr(obj*);
 obj* initialize_init_data_tostring(obj*);
 static bool _G_initialized = false;
@@ -43,8 +42,6 @@ w = initialize_init_data_option_basic(w);
 if (io_result_is_error(w)) return w;
 w = initialize_init_data_uint(w);
 if (io_result_is_error(w)) return w;
-w = initialize_init_data_ordering_basic(w);
-if (io_result_is_error(w)) return w;
 w = initialize_init_data_repr(w);
 if (io_result_is_error(w)) return w;
 w = initialize_init_data_tostring(w);
diff --git a/src/stage0/init/data/default.cpp b/src/stage0/init/data/default.cpp
index 4d5fafeb80..52c3741dd9 100644
--- a/src/stage0/init/data/default.cpp
+++ b/src/stage0/init/data/default.cpp
@@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: init.data.default
-// Imports: init.data.basic init.data.nat.default init.data.char.default init.data.string.default init.data.list.default init.data.int.default init.data.array.default init.data.bytearray.default init.data.fin.default init.data.uint init.data.ordering.default init.data.rbtree.default init.data.rbmap.default init.data.option.basic init.data.option.instances init.data.hashmap.default init.data.random
+// Imports: init.data.basic init.data.nat.default init.data.char.default init.data.string.default init.data.list.default init.data.int.default init.data.array.default init.data.bytearray.default init.data.fin.default init.data.uint init.data.rbtree.default init.data.rbmap.default init.data.option.basic init.data.option.instances init.data.hashmap.default init.data.random
 #include "runtime/object.h"
 #include "runtime/apply.h"
 typedef lean::object obj;    typedef lean::usize  usize;
@@ -24,7 +24,6 @@ obj* initialize_init_data_array_default(obj*);
 obj* initialize_init_data_bytearray_default(obj*);
 obj* initialize_init_data_fin_default(obj*);
 obj* initialize_init_data_uint(obj*);
-obj* initialize_init_data_ordering_default(obj*);
 obj* initialize_init_data_rbtree_default(obj*);
 obj* initialize_init_data_rbmap_default(obj*);
 obj* initialize_init_data_option_basic(obj*);
@@ -56,8 +55,6 @@ w = initialize_init_data_fin_default(w);
 if (io_result_is_error(w)) return w;
 w = initialize_init_data_uint(w);
 if (io_result_is_error(w)) return w;
-w = initialize_init_data_ordering_default(w);
-if (io_result_is_error(w)) return w;
 w = initialize_init_data_rbtree_default(w);
 if (io_result_is_error(w)) return w;
 w = initialize_init_data_rbmap_default(w);
diff --git a/src/stage0/init/data/ordering/basic.cpp b/src/stage0/init/data/ordering/basic.cpp
deleted file mode 100644
index 10481002ba..0000000000
--- a/src/stage0/init/data/ordering/basic.cpp
+++ /dev/null
@@ -1,431 +0,0 @@
-// Lean compiler output
-// Module: init.data.ordering.basic
-// Imports: init.data.repr
-#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_cmp(obj*, obj*);
-obj* l_Ordering_HasRepr___closed__1;
-obj* l_cmp___rarg___boxed(obj*, obj*, obj*);
-obj* l_cmpUsing(obj*, obj*);
-obj* l_Ordering_orElse___boxed(obj*, obj*);
-uint8 l_Ordering_orElse___main(uint8, uint8);
-obj* l_Ordering_HasRepr(uint8);
-obj* l_Ordering_orElse___main___boxed(obj*, obj*);
-uint8 l_Ordering_swap___main(uint8);
-obj* l_cmpUsing___rarg___boxed(obj*, obj*, obj*);
-obj* l_Ordering_HasRepr___boxed(obj*);
-obj* l_Ordering_HasRepr___closed__3;
-obj* l_Ordering_swap___main___boxed(obj*);
-uint8 l_cmpUsing___rarg(obj*, obj*, obj*);
-uint8 l_Ordering_swap(uint8);
-obj* l_Ordering_HasRepr___closed__2;
-obj* l_Ordering_DecidableEq___boxed(obj*, obj*);
-obj* l_cmpUsing___boxed(obj*, obj*);
-uint8 l_Ordering_DecidableEq(uint8, uint8);
-uint8 l_cmp___rarg(obj*, obj*, obj*);
-uint8 l_Ordering_orElse(uint8, uint8);
-obj* l_Ordering_swap___boxed(obj*);
-obj* l_cmp___boxed(obj*, obj*);
-obj* _init_l_Ordering_HasRepr___closed__1() {
-_start:
-{
-obj* x_1; 
-x_1 = lean::mk_string("lt");
-return x_1;
-}
-}
-obj* _init_l_Ordering_HasRepr___closed__2() {
-_start:
-{
-obj* x_1; 
-x_1 = lean::mk_string("Eq");
-return x_1;
-}
-}
-obj* _init_l_Ordering_HasRepr___closed__3() {
-_start:
-{
-obj* x_1; 
-x_1 = lean::mk_string("gt");
-return x_1;
-}
-}
-obj* l_Ordering_HasRepr(uint8 x_1) {
-_start:
-{
-switch (x_1) {
-case 0:
-{
-obj* x_2; 
-x_2 = l_Ordering_HasRepr___closed__1;
-return x_2;
-}
-case 1:
-{
-obj* x_3; 
-x_3 = l_Ordering_HasRepr___closed__2;
-return x_3;
-}
-default: 
-{
-obj* x_4; 
-x_4 = l_Ordering_HasRepr___closed__3;
-return x_4;
-}
-}
-}
-}
-obj* l_Ordering_HasRepr___boxed(obj* x_1) {
-_start:
-{
-uint8 x_2; obj* x_3; 
-x_2 = lean::unbox(x_1);
-lean::dec(x_1);
-x_3 = l_Ordering_HasRepr(x_2);
-return x_3;
-}
-}
-uint8 l_Ordering_swap___main(uint8 x_1) {
-_start:
-{
-switch (x_1) {
-case 0:
-{
-uint8 x_2; 
-x_2 = 2;
-return x_2;
-}
-case 1:
-{
-return x_1;
-}
-default: 
-{
-uint8 x_3; 
-x_3 = 0;
-return x_3;
-}
-}
-}
-}
-obj* l_Ordering_swap___main___boxed(obj* x_1) {
-_start:
-{
-uint8 x_2; uint8 x_3; obj* x_4; 
-x_2 = lean::unbox(x_1);
-lean::dec(x_1);
-x_3 = l_Ordering_swap___main(x_2);
-x_4 = lean::box(x_3);
-return x_4;
-}
-}
-uint8 l_Ordering_swap(uint8 x_1) {
-_start:
-{
-uint8 x_2; 
-x_2 = l_Ordering_swap___main(x_1);
-return x_2;
-}
-}
-obj* l_Ordering_swap___boxed(obj* x_1) {
-_start:
-{
-uint8 x_2; uint8 x_3; obj* x_4; 
-x_2 = lean::unbox(x_1);
-lean::dec(x_1);
-x_3 = l_Ordering_swap(x_2);
-x_4 = lean::box(x_3);
-return x_4;
-}
-}
-uint8 l_Ordering_orElse___main(uint8 x_1, uint8 x_2) {
-_start:
-{
-obj* x_3; 
-x_3 = lean::box(x_1);
-if (lean::obj_tag(x_3) == 1)
-{
-return x_2;
-}
-else
-{
-lean::dec(x_3);
-return x_1;
-}
-}
-}
-obj* l_Ordering_orElse___main___boxed(obj* x_1, obj* x_2) {
-_start:
-{
-uint8 x_3; uint8 x_4; uint8 x_5; obj* x_6; 
-x_3 = lean::unbox(x_1);
-lean::dec(x_1);
-x_4 = lean::unbox(x_2);
-lean::dec(x_2);
-x_5 = l_Ordering_orElse___main(x_3, x_4);
-x_6 = lean::box(x_5);
-return x_6;
-}
-}
-uint8 l_Ordering_orElse(uint8 x_1, uint8 x_2) {
-_start:
-{
-obj* x_3; 
-x_3 = lean::box(x_1);
-if (lean::obj_tag(x_3) == 1)
-{
-return x_2;
-}
-else
-{
-lean::dec(x_3);
-return x_1;
-}
-}
-}
-obj* l_Ordering_orElse___boxed(obj* x_1, obj* x_2) {
-_start:
-{
-uint8 x_3; uint8 x_4; uint8 x_5; obj* x_6; 
-x_3 = lean::unbox(x_1);
-lean::dec(x_1);
-x_4 = lean::unbox(x_2);
-lean::dec(x_2);
-x_5 = l_Ordering_orElse(x_3, x_4);
-x_6 = lean::box(x_5);
-return x_6;
-}
-}
-uint8 l_cmpUsing___rarg(obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; uint8 x_5; 
-lean::inc(x_1);
-lean::inc(x_3);
-lean::inc(x_2);
-x_4 = lean::apply_2(x_1, x_2, x_3);
-x_5 = lean::unbox(x_4);
-lean::dec(x_4);
-if (x_5 == 0)
-{
-obj* x_6; uint8 x_7; 
-x_6 = lean::apply_2(x_1, x_3, x_2);
-x_7 = lean::unbox(x_6);
-lean::dec(x_6);
-if (x_7 == 0)
-{
-uint8 x_8; 
-x_8 = 1;
-return x_8;
-}
-else
-{
-uint8 x_9; 
-x_9 = 2;
-return x_9;
-}
-}
-else
-{
-uint8 x_10; 
-lean::dec(x_3);
-lean::dec(x_2);
-lean::dec(x_1);
-x_10 = 0;
-return x_10;
-}
-}
-}
-obj* l_cmpUsing(obj* x_1, obj* x_2) {
-_start:
-{
-obj* x_3; 
-x_3 = lean::alloc_closure(reinterpret_cast<void*>(l_cmpUsing___rarg___boxed), 3, 0);
-return x_3;
-}
-}
-obj* l_cmpUsing___rarg___boxed(obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-uint8 x_4; obj* x_5; 
-x_4 = l_cmpUsing___rarg(x_1, x_2, x_3);
-x_5 = lean::box(x_4);
-return x_5;
-}
-}
-obj* l_cmpUsing___boxed(obj* x_1, obj* x_2) {
-_start:
-{
-obj* x_3; 
-x_3 = l_cmpUsing(x_1, x_2);
-lean::dec(x_2);
-return x_3;
-}
-}
-uint8 l_cmp___rarg(obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-obj* x_4; uint8 x_5; 
-lean::inc(x_1);
-lean::inc(x_3);
-lean::inc(x_2);
-x_4 = lean::apply_2(x_1, x_2, x_3);
-x_5 = lean::unbox(x_4);
-lean::dec(x_4);
-if (x_5 == 0)
-{
-obj* x_6; uint8 x_7; 
-x_6 = lean::apply_2(x_1, x_3, x_2);
-x_7 = lean::unbox(x_6);
-lean::dec(x_6);
-if (x_7 == 0)
-{
-uint8 x_8; 
-x_8 = 1;
-return x_8;
-}
-else
-{
-uint8 x_9; 
-x_9 = 2;
-return x_9;
-}
-}
-else
-{
-uint8 x_10; 
-lean::dec(x_3);
-lean::dec(x_2);
-lean::dec(x_1);
-x_10 = 0;
-return x_10;
-}
-}
-}
-obj* l_cmp(obj* x_1, obj* x_2) {
-_start:
-{
-obj* x_3; 
-x_3 = lean::alloc_closure(reinterpret_cast<void*>(l_cmp___rarg___boxed), 3, 0);
-return x_3;
-}
-}
-obj* l_cmp___rarg___boxed(obj* x_1, obj* x_2, obj* x_3) {
-_start:
-{
-uint8 x_4; obj* x_5; 
-x_4 = l_cmp___rarg(x_1, x_2, x_3);
-x_5 = lean::box(x_4);
-return x_5;
-}
-}
-obj* l_cmp___boxed(obj* x_1, obj* x_2) {
-_start:
-{
-obj* x_3; 
-x_3 = l_cmp(x_1, x_2);
-lean::dec(x_2);
-return x_3;
-}
-}
-uint8 l_Ordering_DecidableEq(uint8 x_1, uint8 x_2) {
-_start:
-{
-switch (x_1) {
-case 0:
-{
-obj* x_3; 
-x_3 = lean::box(x_2);
-if (lean::obj_tag(x_3) == 0)
-{
-uint8 x_4; 
-x_4 = 1;
-return x_4;
-}
-else
-{
-uint8 x_5; 
-lean::dec(x_3);
-x_5 = 0;
-return x_5;
-}
-}
-case 1:
-{
-obj* x_6; 
-x_6 = lean::box(x_2);
-if (lean::obj_tag(x_6) == 1)
-{
-uint8 x_7; 
-x_7 = 1;
-return x_7;
-}
-else
-{
-uint8 x_8; 
-lean::dec(x_6);
-x_8 = 0;
-return x_8;
-}
-}
-default: 
-{
-obj* x_9; 
-x_9 = lean::box(x_2);
-if (lean::obj_tag(x_9) == 2)
-{
-uint8 x_10; 
-x_10 = 1;
-return x_10;
-}
-else
-{
-uint8 x_11; 
-lean::dec(x_9);
-x_11 = 0;
-return x_11;
-}
-}
-}
-}
-}
-obj* l_Ordering_DecidableEq___boxed(obj* x_1, obj* x_2) {
-_start:
-{
-uint8 x_3; uint8 x_4; uint8 x_5; obj* x_6; 
-x_3 = lean::unbox(x_1);
-lean::dec(x_1);
-x_4 = lean::unbox(x_2);
-lean::dec(x_2);
-x_5 = l_Ordering_DecidableEq(x_3, x_4);
-x_6 = lean::box(x_5);
-return x_6;
-}
-}
-obj* initialize_init_data_repr(obj*);
-static bool _G_initialized = false;
-obj* initialize_init_data_ordering_basic(obj* w) {
-if (_G_initialized) return w;
-_G_initialized = true;
-if (io_result_is_error(w)) return w;
-w = initialize_init_data_repr(w);
-if (io_result_is_error(w)) return w;
-l_Ordering_HasRepr___closed__1 = _init_l_Ordering_HasRepr___closed__1();
-lean::mark_persistent(l_Ordering_HasRepr___closed__1);
-l_Ordering_HasRepr___closed__2 = _init_l_Ordering_HasRepr___closed__2();
-lean::mark_persistent(l_Ordering_HasRepr___closed__2);
-l_Ordering_HasRepr___closed__3 = _init_l_Ordering_HasRepr___closed__3();
-lean::mark_persistent(l_Ordering_HasRepr___closed__3);
-return w;
-}
diff --git a/src/stage0/init/data/ordering/default.cpp b/src/stage0/init/data/ordering/default.cpp
deleted file mode 100644
index e501b6df23..0000000000
--- a/src/stage0/init/data/ordering/default.cpp
+++ /dev/null
@@ -1,26 +0,0 @@
-// Lean compiler output
-// Module: init.data.ordering.default
-// Imports: init.data.ordering.basic
-#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* initialize_init_data_ordering_basic(obj*);
-static bool _G_initialized = false;
-obj* initialize_init_data_ordering_default(obj* w) {
-if (_G_initialized) return w;
-_G_initialized = true;
-if (io_result_is_error(w)) return w;
-w = initialize_init_data_ordering_basic(w);
-if (io_result_is_error(w)) return w;
-return w;
-}
diff --git a/src/stage0/init/lean/syntax.cpp b/src/stage0/init/lean/syntax.cpp
index 529679f8ed..9ea5c6f5be 100644
--- a/src/stage0/init/lean/syntax.cpp
+++ b/src/stage0/init/lean/syntax.cpp
@@ -36,6 +36,7 @@ obj* nat_sub(obj*, obj*);
 obj* l_Lean_Syntax_ifNode(obj*, obj*);
 obj* l_Lean_nullKind___closed__2;
 obj* l_Lean_stxInh(obj*);
+obj* l_Lean_Syntax_setArg(obj*);
 extern obj* l_Lean_Format_paren___closed__2;
 obj* l_Lean_unreachIsNodeOther(obj*, obj*, obj*, obj*);
 obj* l___private_init_lean_syntax_4__reprintLeaf(obj*, obj*);
@@ -78,6 +79,7 @@ obj* l___private_init_lean_syntax_7__decodeHexLitAux___main(obj*, obj*, obj*);
 extern obj* l_Lean_Format_sbracket___closed__1;
 obj* l___private_init_lean_syntax_2__updateLeadingAux___main___rarg(obj*, obj*);
 obj* l_Lean_SyntaxNode_getNumArgs___rarg(obj*);
+obj* l_Lean_Syntax_modifyArg___rarg(obj*, obj*, obj*);
 obj* l_Lean_charLitKind___closed__2;
 obj* l_Lean_Syntax_asNode___main___rarg___boxed(obj*);
 obj* l_Lean_Syntax_setTailInfo(obj*);
@@ -107,6 +109,7 @@ obj* l_Lean_Syntax_formatStx___main___rarg___closed__3;
 obj* l_Lean_Syntax_formatStx___rarg(obj*);
 extern obj* l_Lean_Format_sbracket___closed__2;
 obj* l___private_init_lean_syntax_4__reprintLeaf___main___boxed(obj*, obj*);
+obj* l_Lean_Syntax_setArg___rarg(obj*, obj*, obj*);
 obj* l_Lean_Syntax_isStrLit___main(obj*);
 obj* l_Lean_Syntax_isOfKind___main___rarg___boxed(obj*, obj*);
 obj* l_Array_mfindRevAux___main___at_Lean_Syntax_getTailInfo___main___spec__1___rarg___boxed(obj*, obj*, obj*);
@@ -207,6 +210,7 @@ obj* l_Lean_strLitKind;
 obj* l_Lean_Syntax_isOfKind___rarg___boxed(obj*, obj*);
 obj* l_Lean_Syntax_asNode___main___rarg(obj*);
 obj* l_List_map___main___at_Lean_Syntax_formatStx___main___spec__1___rarg(obj*);
+obj* l_Lean_Syntax_setArgs(obj*);
 obj* l_Lean_choiceKind___closed__2;
 obj* l___private_init_lean_syntax_4__reprintLeaf___boxed(obj*, obj*);
 obj* l_Lean_Syntax_reprint(obj*);
@@ -215,6 +219,7 @@ obj* l_Lean_Syntax_getHeadInfo(obj*);
 namespace lean {
 uint32 string_utf8_get(obj*, obj*);
 }
+obj* l_Lean_Syntax_modifyArg(obj*);
 obj* l_Lean_Syntax_mreplace___rarg(obj*, obj*, obj*);
 obj* l_Lean_unreachIsNodeMissing(obj*, obj*, obj*);
 obj* l_Array_ummapAux___main___at_Lean_Syntax_mrewriteBottomUp___main___spec__1___rarg(obj*, obj*, obj*, obj*);
@@ -236,7 +241,6 @@ obj* l___private_init_lean_syntax_7__decodeHexLitAux(obj*, obj*, obj*);
 obj* l_Lean_Syntax_isIdent(obj*);
 obj* l_Array_mfindAux___main___at_Lean_Syntax_getHeadInfo___main___spec__1(obj*);
 obj* l_Lean_Syntax_mrewriteBottomUp___main___at_Lean_Syntax_rewriteBottomUp___spec__1___rarg(obj*, obj*);
-obj* l_Lean_SyntaxNode_updateArgs(obj*);
 obj* l___private_init_lean_syntax_5__decodeBinLitAux(obj*, obj*, obj*);
 obj* l_Lean_Syntax_reprint___rarg___boxed(obj*);
 obj* l___private_init_lean_syntax_5__decodeBinLitAux___main___boxed(obj*, obj*, obj*);
@@ -247,11 +251,14 @@ obj* l_Lean_SyntaxNode_getKind___rarg___boxed(obj*);
 obj* l_Lean_Syntax_getId___main___rarg___boxed(obj*);
 obj* l_Lean_Format_joinSep___main___at_Lean_Syntax_formatStx___main___spec__2___boxed(obj*, obj*);
 obj* l_Lean_SyntaxNode_getArg___rarg___boxed(obj*, obj*);
+obj* l_Lean_Syntax_setArgs___rarg(obj*, obj*);
 obj* l___private_init_lean_syntax_1__updateInfo(obj*, obj*);
 obj* l___private_init_lean_syntax_8__decodeDecimalLitAux___main___boxed(obj*, obj*, obj*);
 uint8 l_Char_isDigit(uint32);
 uint8 l_Lean_Syntax_isOfKind___main___rarg(obj*, obj*);
+obj* l_Lean_Syntax_modifyArgs___rarg(obj*, obj*);
 obj* l___private_init_lean_syntax_3__updateLast___main___at_Lean_Syntax_setTailInfoAux___main___spec__1___rarg(obj*, obj*, obj*);
+obj* l_Lean_Syntax_modifyArgs(obj*);
 obj* l_Array_ummapAux___main___at_Lean_Syntax_mrewriteBottomUp___main___spec__1___rarg___lambda__1___boxed(obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l___private_init_lean_syntax_3__updateLast___main___rarg(obj*, obj*, obj*, obj*);
 obj* l_Lean_Syntax_getIdAt___rarg___boxed(obj*, obj*);
@@ -297,7 +304,6 @@ obj* l_Array_ummapAux___main___at_Lean_Syntax_mreplace___main___spec__1___rarg(o
 obj* l_Lean_Syntax_isMissing___main___rarg___boxed(obj*);
 obj* l_Lean_Syntax_isNatLitAux___main___rarg___boxed(obj*, obj*);
 obj* l_Lean_Syntax_getId___rarg___boxed(obj*);
-obj* l_Lean_SyntaxNode_updateArgs___rarg(obj*, obj*);
 obj* l_Lean_Syntax_formatStx___main___rarg___closed__5;
 obj* l_Lean_unreachIsNodeAtom___boxed(obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_Syntax_isFieldIdx___rarg(obj*);
@@ -315,6 +321,7 @@ obj* string_utf8_extract(obj*, obj*, obj*);
 }
 obj* l_Lean_Syntax_ifNodeKind___rarg___boxed(obj*, obj*, obj*, obj*);
 obj* l_Array_mfindRevAux___main___at_Lean_Syntax_getTailInfo___main___spec__1___rarg(obj*, obj*, obj*);
+obj* l_Lean_SyntaxNode_modifyArgs___rarg(obj*, obj*);
 obj* l_Lean_Syntax_getPos___rarg(obj*);
 namespace lean {
 obj* string_utf8_byte_size(obj*);
@@ -331,6 +338,7 @@ obj* l_Array_set(obj*, obj*, obj*, obj*);
 obj* l_Lean_Syntax_isStrLit___rarg___boxed(obj*);
 obj* l_Lean_Syntax_HasToString___closed__1;
 obj* l___private_init_lean_syntax_7__decodeHexLitAux___boxed(obj*, obj*, obj*);
+obj* l_Lean_SyntaxNode_modifyArgs(obj*);
 obj* l_Lean_strLitKind___closed__2;
 obj* l_Lean_Syntax_formatStx___main___rarg___closed__7;
 obj* l_String_quote(obj*);
@@ -358,7 +366,9 @@ obj* nat_mul(obj*, obj*);
 obj* l_Lean_Syntax_isIdOrAtom___main(obj*);
 obj* l___private_init_lean_syntax_5__decodeBinLitAux___boxed(obj*, obj*, obj*);
 obj* l_Lean_Syntax_mrewriteBottomUp___main___at_Lean_Syntax_rewriteBottomUp___spec__1(obj*);
+obj* l_Lean_Syntax_modifyArg___rarg___boxed(obj*, obj*, obj*);
 obj* l_Lean_Syntax_getTailInfo___rarg___boxed(obj*);
+obj* l_Lean_Syntax_setArg___rarg___boxed(obj*, obj*, obj*);
 obj* l_Lean_Syntax_formatStx___main___rarg___closed__4;
 obj* l_Lean_charLitKind;
 obj* l_Lean_Syntax_mrewriteBottomUp___main___boxed(obj*, obj*);
@@ -1058,7 +1068,7 @@ lean::dec(x_1);
 return x_2;
 }
 }
-obj* l_Lean_SyntaxNode_updateArgs___rarg(obj* x_1, obj* x_2) {
+obj* l_Lean_SyntaxNode_modifyArgs___rarg(obj* x_1, obj* x_2) {
 _start:
 {
 uint8 x_3; 
@@ -1087,11 +1097,11 @@ return x_9;
 }
 }
 }
-obj* l_Lean_SyntaxNode_updateArgs(obj* x_1) {
+obj* l_Lean_SyntaxNode_modifyArgs(obj* x_1) {
 _start:
 {
 obj* x_2; 
-x_2 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_SyntaxNode_updateArgs___rarg), 2, 0);
+x_2 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_SyntaxNode_modifyArgs___rarg), 2, 0);
 return x_2;
 }
 }
@@ -1582,6 +1592,237 @@ lean::dec(x_1);
 return x_3;
 }
 }
+obj* l_Lean_Syntax_setArgs___rarg(obj* x_1, obj* x_2) {
+_start:
+{
+if (lean::obj_tag(x_1) == 1)
+{
+uint8 x_3; 
+x_3 = !lean::is_exclusive(x_1);
+if (x_3 == 0)
+{
+obj* x_4; 
+x_4 = lean::cnstr_get(x_1, 1);
+lean::dec(x_4);
+lean::cnstr_set(x_1, 1, x_2);
+return x_1;
+}
+else
+{
+obj* x_5; obj* x_6; 
+x_5 = lean::cnstr_get(x_1, 0);
+lean::inc(x_5);
+lean::dec(x_1);
+x_6 = lean::alloc_cnstr(1, 2, 0);
+lean::cnstr_set(x_6, 0, x_5);
+lean::cnstr_set(x_6, 1, x_2);
+return x_6;
+}
+}
+else
+{
+lean::dec(x_2);
+return x_1;
+}
+}
+}
+obj* l_Lean_Syntax_setArgs(obj* x_1) {
+_start:
+{
+obj* x_2; 
+x_2 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Syntax_setArgs___rarg), 2, 0);
+return x_2;
+}
+}
+obj* l_Lean_Syntax_modifyArgs___rarg(obj* x_1, obj* x_2) {
+_start:
+{
+if (lean::obj_tag(x_1) == 1)
+{
+uint8 x_3; 
+x_3 = !lean::is_exclusive(x_1);
+if (x_3 == 0)
+{
+obj* x_4; obj* x_5; 
+x_4 = lean::cnstr_get(x_1, 1);
+x_5 = lean::apply_1(x_2, x_4);
+lean::cnstr_set(x_1, 1, x_5);
+return x_1;
+}
+else
+{
+obj* x_6; obj* x_7; obj* x_8; obj* x_9; 
+x_6 = lean::cnstr_get(x_1, 0);
+x_7 = lean::cnstr_get(x_1, 1);
+lean::inc(x_7);
+lean::inc(x_6);
+lean::dec(x_1);
+x_8 = lean::apply_1(x_2, x_7);
+x_9 = lean::alloc_cnstr(1, 2, 0);
+lean::cnstr_set(x_9, 0, x_6);
+lean::cnstr_set(x_9, 1, x_8);
+return x_9;
+}
+}
+else
+{
+lean::dec(x_2);
+return x_1;
+}
+}
+}
+obj* l_Lean_Syntax_modifyArgs(obj* x_1) {
+_start:
+{
+obj* x_2; 
+x_2 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Syntax_modifyArgs___rarg), 2, 0);
+return x_2;
+}
+}
+obj* l_Lean_Syntax_setArg___rarg(obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+if (lean::obj_tag(x_1) == 1)
+{
+uint8 x_4; 
+x_4 = !lean::is_exclusive(x_1);
+if (x_4 == 0)
+{
+obj* x_5; obj* x_6; 
+x_5 = lean::cnstr_get(x_1, 1);
+x_6 = lean::array_set(x_5, x_2, x_3);
+lean::cnstr_set(x_1, 1, x_6);
+return x_1;
+}
+else
+{
+obj* x_7; obj* x_8; obj* x_9; obj* x_10; 
+x_7 = lean::cnstr_get(x_1, 0);
+x_8 = lean::cnstr_get(x_1, 1);
+lean::inc(x_8);
+lean::inc(x_7);
+lean::dec(x_1);
+x_9 = lean::array_set(x_8, x_2, x_3);
+x_10 = lean::alloc_cnstr(1, 2, 0);
+lean::cnstr_set(x_10, 0, x_7);
+lean::cnstr_set(x_10, 1, x_9);
+return x_10;
+}
+}
+else
+{
+lean::dec(x_3);
+return x_1;
+}
+}
+}
+obj* l_Lean_Syntax_setArg(obj* x_1) {
+_start:
+{
+obj* x_2; 
+x_2 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Syntax_setArg___rarg___boxed), 3, 0);
+return x_2;
+}
+}
+obj* l_Lean_Syntax_setArg___rarg___boxed(obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+obj* x_4; 
+x_4 = l_Lean_Syntax_setArg___rarg(x_1, x_2, x_3);
+lean::dec(x_2);
+return x_4;
+}
+}
+obj* l_Lean_Syntax_modifyArg___rarg(obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+if (lean::obj_tag(x_1) == 1)
+{
+uint8 x_4; 
+x_4 = !lean::is_exclusive(x_1);
+if (x_4 == 0)
+{
+obj* x_5; obj* x_6; uint8 x_7; 
+x_5 = lean::cnstr_get(x_1, 1);
+x_6 = lean::array_get_size(x_5);
+x_7 = lean::nat_dec_lt(x_2, x_6);
+lean::dec(x_6);
+if (x_7 == 0)
+{
+lean::dec(x_3);
+return x_1;
+}
+else
+{
+obj* x_8; obj* x_9; obj* x_10; obj* x_11; obj* x_12; 
+x_8 = lean::array_fget(x_5, x_2);
+x_9 = lean::box(0);
+x_10 = lean::array_fset(x_5, x_2, x_9);
+x_11 = lean::apply_1(x_3, x_8);
+x_12 = lean::array_fset(x_10, x_2, x_11);
+lean::cnstr_set(x_1, 1, x_12);
+return x_1;
+}
+}
+else
+{
+obj* x_13; obj* x_14; obj* x_15; uint8 x_16; 
+x_13 = lean::cnstr_get(x_1, 0);
+x_14 = lean::cnstr_get(x_1, 1);
+lean::inc(x_14);
+lean::inc(x_13);
+lean::dec(x_1);
+x_15 = lean::array_get_size(x_14);
+x_16 = lean::nat_dec_lt(x_2, x_15);
+lean::dec(x_15);
+if (x_16 == 0)
+{
+obj* x_17; 
+lean::dec(x_3);
+x_17 = lean::alloc_cnstr(1, 2, 0);
+lean::cnstr_set(x_17, 0, x_13);
+lean::cnstr_set(x_17, 1, x_14);
+return x_17;
+}
+else
+{
+obj* x_18; obj* x_19; obj* x_20; obj* x_21; obj* x_22; obj* x_23; 
+x_18 = lean::array_fget(x_14, x_2);
+x_19 = lean::box(0);
+x_20 = lean::array_fset(x_14, x_2, x_19);
+x_21 = lean::apply_1(x_3, x_18);
+x_22 = lean::array_fset(x_20, x_2, x_21);
+x_23 = lean::alloc_cnstr(1, 2, 0);
+lean::cnstr_set(x_23, 0, x_13);
+lean::cnstr_set(x_23, 1, x_22);
+return x_23;
+}
+}
+}
+else
+{
+lean::dec(x_3);
+return x_1;
+}
+}
+}
+obj* l_Lean_Syntax_modifyArg(obj* x_1) {
+_start:
+{
+obj* x_2; 
+x_2 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Syntax_modifyArg___rarg___boxed), 3, 0);
+return x_2;
+}
+}
+obj* l_Lean_Syntax_modifyArg___rarg___boxed(obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+obj* x_4; 
+x_4 = l_Lean_Syntax_modifyArg___rarg(x_1, x_2, x_3);
+lean::dec(x_2);
+return x_4;
+}
+}
 obj* l_Lean_Syntax_getIdAt___rarg(obj* x_1, obj* x_2) {
 _start:
 {