diff --git a/library/init/lean/ir/extract_cpp.lean b/library/init/lean/ir/extract_cpp.lean
index 93c3f84beb..3713ff945d 100644
--- a/library/init/lean/ir/extract_cpp.lean
+++ b/library/init/lean/ir/extract_cpp.lean
@@ -293,7 +293,7 @@ do env ← read,
      let fname := if arity > closure_max_args then "uncurry" ++ fname else fname,
      emit "reinterpret_cast<lean::lean_cfun>(" >> emit fname >> emit ")" <+> emit arity <+> emit ys.length,
      emit ")",
-     ys.mfoldl (λ i y, emit ";\nlean::set_closure_arg" >> paren (emit_var x <+> emit i <+> emit_var y) >> return (i+1)) 0,
+     ys.mfoldl (λ i y, emit ";\nlean::closure_set_arg" >> paren (emit_var x <+> emit i <+> emit_var y) >> return (i+1)) 0,
      return ()
    | none   := throw "invalid closure"
 
@@ -310,9 +310,9 @@ ins.decorate_error $
    if c then emit_global f
    else (emit_fnid f >> paren(emit_var_list ys))
  | (instr.cnstr o t n sz)    := emit_var o >> emit " = lean::alloc_cnstr" >> paren(emit t <+> emit n <+> emit sz)
- | (instr.set o i x)         := emit "lean::set_cnstr_obj" >> paren (emit_var o <+> emit i <+> emit_var x)
+ | (instr.set o i x)         := emit "lean::cnstr_set_obj" >> paren (emit_var o <+> emit i <+> emit_var x)
  | (instr.get x o i)         := emit_var x >> emit " = lean::cnstr_obj" >> paren(emit_var o <+> emit i)
- | (instr.sset o d x)        := emit "lean::set_cnstr_scalar" >> paren(emit_var o <+> emit d <+> emit_var x)
+ | (instr.sset o d x)        := emit "lean::cnstr_set_scalar" >> paren(emit_var o <+> emit d <+> emit_var x)
  | (instr.sget x t o d)      := emit_var x >> emit " = lean::cnstr_scalar" >> emit_template_param t >> paren(emit_var o <+> emit d)
  | (instr.closure x f ys)    := emit_closure x f ys
  | (instr.apply x ys)        := emit_apply x ys
@@ -321,8 +321,8 @@ ins.decorate_error $
  | (instr.array_write a i v) :=
    do env ← read,
       if env.ctx.find v = some type.object
-      then emit "lean::set_array_obj" >> paren(emit_var a <+> emit_var i <+> emit_var v)
-      else emit "lean::set_sarray_data" >> paren(emit_var a <+> emit_var i <+> emit_var v))
+      then emit "lean::array_set_obj" >> paren(emit_var a <+> emit_var i <+> emit_var v)
+      else emit "lean::sarray_set_data" >> paren(emit_var a <+> emit_var i <+> emit_var v))
 >> emit_eos
 
 def emit_block (b : block) : extract_m unit :=
diff --git a/src/runtime/lean_obj.cpp b/src/runtime/lean_obj.cpp
index 450b96ea15..6da0714401 100644
--- a/src/runtime/lean_obj.cpp
+++ b/src/runtime/lean_obj.cpp
@@ -132,7 +132,7 @@ lean_obj * mk_string(char const * s) {
     size_t len = utf8_strlen(s);
     size_t rsz = sz + sizeof(size_t) + 1;
     lean_obj * r = alloc_sarray(1, rsz, rsz);
-    set_sarray_data<size_t>(r, 0, len);
+    sarray_set_data<size_t>(r, 0, len);
     memcpy(sarray_cptr<char>(r) + sizeof(size_t), s, sz+1);
     return r;
 }
@@ -146,9 +146,9 @@ lean_obj * string_push(lean_obj * s, unsigned c) {
     lean_obj * r = sarray_ensure_capacity(s, 5);
     size_t sz = sarray_size(r);
     unsigned consumed = push_unicode_scalar(sarray_cptr<char>(r) + sz - 1, c);
-    set_sarray_size(r, sz + consumed);
-    set_sarray_data<char>(r, sz + consumed - 1, 0);
-    set_sarray_data<size_t>(r, 0, string_len(r) + 1);
+    sarray_set_size(r, sz + consumed);
+    sarray_set_data<char>(r, sz + consumed - 1, 0);
+    sarray_set_data<size_t>(r, 0, string_len(r) + 1);
     return r;
 }
 
@@ -164,9 +164,9 @@ lean_obj * string_append(lean_obj * s1, lean_obj * s2) {
     if (s1 == s2) s2 = r;
     memcpy(sarray_cptr<char>(r) + sz1 - 1, c_str(s2), sz2 - 1);
     unsigned new_sz = sz1 + sz2 - 1;
-    set_sarray_size(r, new_sz);
-    set_sarray_data<char>(r, new_sz - 1, 0);
-    set_sarray_data<size_t>(r, 0, len1 + len2);
+    sarray_set_size(r, new_sz);
+    sarray_set_data<char>(r, new_sz - 1, 0);
+    sarray_set_data<size_t>(r, 0, len1 + len2);
     return r;
 }
 
diff --git a/src/runtime/lean_obj.h b/src/runtime/lean_obj.h
index 35ef22b025..9e07bf820a 100644
--- a/src/runtime/lean_obj.h
+++ b/src/runtime/lean_obj.h
@@ -195,33 +195,10 @@ inline void dealloc(lean_obj * o) {
     }
 }
 
-/* Getters */
-inline unsigned cnstr_tag(lean_obj * o) { return to_cnstr(o)->m_tag; }
-inline unsigned cnstr_num_objs(lean_obj * o) { return to_cnstr(o)->m_num_objs; }
-inline unsigned cnstr_scalar_size(lean_obj * o) { return to_cnstr(o)->m_scalar_size; }
-inline size_t cnstr_byte_size(lean_obj * o) { return sizeof(lean_cnstr) + cnstr_num_objs(o)*sizeof(lean_obj*) + cnstr_scalar_size(o); } // NOLINT
-
-inline size_t array_size(lean_obj * o) { return to_array(o)->m_size; }
-inline size_t array_capacity(lean_obj * o) { return to_array(o)->m_capacity; }
-inline size_t array_byte_size(lean_obj * o) { return sizeof(lean_array) + array_capacity(o)*sizeof(lean_obj*); } // NOLINT
-
-inline unsigned sarray_elem_size(lean_obj * o) { return to_sarray(o)->m_elem_size; }
-inline size_t sarray_size(lean_obj * o) { return to_sarray(o)->m_size; }
-inline size_t sarray_capacity(lean_obj * o) { return to_sarray(o)->m_capacity; }
-inline size_t sarray_byte_size(lean_obj * o) { return sizeof(lean_sarray) + sarray_capacity(o)*sarray_elem_size(o); } // NOLINT
-
-inline lean_cfun closure_fun(lean_obj * o) { return to_closure(o)->m_fun; }
-inline unsigned closure_arity(lean_obj * o) { return to_closure(o)->m_arity; }
-inline unsigned closure_num_fixed(lean_obj * o) { return to_closure(o)->m_num_fixed; }
-inline size_t closure_byte_size(lean_obj * o) { return sizeof(lean_closure) + (closure_arity(o) - 1)*sizeof(lean_obj*); } // NOLINT
-
-inline mpz const & mpz_value(lean_obj * o) { return to_mpz(o)->m_value; }
-
-inline unsigned tag(lean_obj * o) { if (is_scalar(o)) return unbox(o); else return cnstr_tag(o); }
-
 /* Size of the object in bytes. This function is used for debugging purposes.
    \pre !is_scalar(o) && !is_external(o) */
 size_t obj_byte_size(lean_obj * o);
+
 /* Size of the object header in bytes. This function is used for debugging purposes.
    \pre !is_scalar(o) && !is_external(o) */
 size_t obj_header_size(lean_obj * o);
@@ -234,43 +211,48 @@ inline T obj_data(lean_obj * o, size_t offset) {
     return *(reinterpret_cast<T *>(reinterpret_cast<char *>(o) + offset));
 }
 
+/* Set object data of type T */
+template<typename T>
+inline void obj_set_data(lean_obj * o, size_t offset, T v) {
+    lean_assert(!is_shared(o));
+    lean_assert(obj_header_size(o) <= offset);
+    lean_assert(offset + sizeof(T) <= obj_byte_size(o));
+    *(reinterpret_cast<T *>(reinterpret_cast<char *>(o) + offset)) = v;
+}
+
+/* Constructor objects */
+
+inline unsigned cnstr_tag(lean_obj * o) { return to_cnstr(o)->m_tag; }
+inline unsigned cnstr_num_objs(lean_obj * o) { return to_cnstr(o)->m_num_objs; }
+inline unsigned cnstr_scalar_size(lean_obj * o) { return to_cnstr(o)->m_scalar_size; }
+inline size_t cnstr_byte_size(lean_obj * o) { return sizeof(lean_cnstr) + cnstr_num_objs(o)*sizeof(lean_obj*) + cnstr_scalar_size(o); } // NOLINT
 inline lean_obj * cnstr_obj(lean_obj * o, unsigned i) {
     lean_assert(i < cnstr_num_objs(o));
     return obj_data<lean_obj*>(o, sizeof(lean_cnstr) + sizeof(lean_obj*)*i); // NOLINT
 }
-
 inline lean_obj ** cnstr_obj_cptr(lean_obj * o) {
     lean_assert(is_cnstr(o));
     return reinterpret_cast<lean_obj**>(reinterpret_cast<char*>(o) + sizeof(lean_cnstr));
 }
-
 template<typename T>
 inline T cnstr_scalar(lean_obj * o, size_t offset) {
     return obj_data<T>(o, sizeof(lean_cnstr) + offset);
 }
-
-inline lean_obj * array_obj(lean_obj * o, size_t i) {
-    lean_assert(i < array_size(o));
-    return obj_data<lean_obj*>(o, sizeof(lean_array) + sizeof(lean_obj*)*i); // NOLINT
+inline void cnstr_set_obj(lean_obj * o, unsigned i, lean_obj * v) {
+    lean_assert(i < cnstr_num_objs(o));
+    obj_set_data(o, sizeof(lean_cnstr) + sizeof(lean_obj*)*i, v); // NOLINT
 }
-
-inline lean_obj ** array_cptr(lean_obj * o) {
-    lean_assert(is_array(o));
-    return reinterpret_cast<lean_obj**>(reinterpret_cast<char*>(o) + sizeof(lean_array));
-}
-
 template<typename T>
-inline T * sarray_cptr(lean_obj * o) {
-    lean_assert(is_sarray(o));
-    lean_assert(sarray_elem_size(o) == sizeof(T));
-    return reinterpret_cast<T*>(reinterpret_cast<char*>(o) + sizeof(lean_sarray));
+inline void cnstr_set_scalar(lean_obj * o, unsigned i, T v) {
+    obj_set_data(o, sizeof(lean_cnstr) + i, v);
 }
 
-template<typename T>
-T sarray_data(lean_obj * o, size_t i) {
-    return sarray_cptr<T>(o)[i];
-}
+/* Closures */
 
+inline lean_cfun closure_fun(lean_obj * o) { return to_closure(o)->m_fun; }
+inline unsigned closure_arity(lean_obj * o) { return to_closure(o)->m_arity; }
+inline unsigned closure_num_fixed(lean_obj * o) { return to_closure(o)->m_num_fixed; }
+inline size_t closure_byte_size(lean_obj * o) { return sizeof(lean_closure) + (closure_arity(o) - 1)*sizeof(lean_obj*); } // NOLINT
 inline lean_obj * closure_arg(lean_obj * o, unsigned i) {
     lean_assert(i < closure_num_fixed(o));
     return obj_data<lean_obj*>(o, sizeof(lean_closure) + sizeof(lean_obj*)*i); // NOLINT
@@ -280,64 +262,61 @@ inline lean_obj ** closure_arg_cptr(lean_obj * o) {
     lean_assert(is_closure(o));
     return reinterpret_cast<lean_obj**>(reinterpret_cast<char*>(o) + sizeof(lean_closure));
 }
-
-/* Low level setters.
-   Remark: the set_*_obj procedures do *NOT* update reference counters. */
-
-template<typename T>
-inline void set_obj_data(lean_obj * o, size_t offset, T v) {
-    lean_assert(!is_shared(o));
-    lean_assert(obj_header_size(o) <= offset);
-    lean_assert(offset + sizeof(T) <= obj_byte_size(o));
-    *(reinterpret_cast<T *>(reinterpret_cast<char *>(o) + offset)) = v;
+inline void closure_set_arg(lean_obj * o, unsigned i, lean_obj * a) {
+    lean_assert(i < closure_num_fixed(o));
+    obj_set_data(o, sizeof(lean_closure) + sizeof(lean_obj*)*i, a); // NOLINT
 }
+inline unsigned tag(lean_obj * o) { if (is_scalar(o)) return unbox(o); else return cnstr_tag(o); }
 
-inline void set_cnstr_obj(lean_obj * o, unsigned i, lean_obj * v) {
-    lean_assert(i < cnstr_num_objs(o));
-    set_obj_data(o, sizeof(lean_cnstr) + sizeof(lean_obj*)*i, v); // NOLINT
+/* Array of objects */
+
+inline size_t array_size(lean_obj * o) { return to_array(o)->m_size; }
+inline size_t array_capacity(lean_obj * o) { return to_array(o)->m_capacity; }
+inline size_t array_byte_size(lean_obj * o) { return sizeof(lean_array) + array_capacity(o)*sizeof(lean_obj*); } // NOLINT
+inline lean_obj * array_obj(lean_obj * o, size_t i) {
+    lean_assert(i < array_size(o));
+    return obj_data<lean_obj*>(o, sizeof(lean_array) + sizeof(lean_obj*)*i); // NOLINT
 }
-
-template<typename T>
-inline void set_cnstr_scalar(lean_obj * o, unsigned i, T v) {
-    set_obj_data(o, sizeof(lean_cnstr) + i, v);
+inline lean_obj ** array_cptr(lean_obj * o) {
+    lean_assert(is_array(o));
+    return reinterpret_cast<lean_obj**>(reinterpret_cast<char*>(o) + sizeof(lean_array));
 }
-
-inline void set_array_size(lean_obj * o, size_t sz) {
+inline void array_set_size(lean_obj * o, size_t sz) {
     lean_assert(is_array(o));
     lean_assert(!is_shared(o));
     lean_assert(sz <= array_capacity(o));
     to_array(o)->m_size = sz;
 }
-
-inline void set_array_obj(lean_obj * o, size_t i, lean_obj * v) {
+inline void array_set_obj(lean_obj * o, size_t i, lean_obj * v) {
     lean_assert(i < array_size(o));
-    set_obj_data(o, sizeof(lean_array) + sizeof(lean_obj*)*i, v); // NOLINT
+    obj_set_data(o, sizeof(lean_array) + sizeof(lean_obj*)*i, v); // NOLINT
 }
 
+/* Array of scalars */
+
+inline unsigned sarray_elem_size(lean_obj * o) { return to_sarray(o)->m_elem_size; }
+inline size_t sarray_size(lean_obj * o) { return to_sarray(o)->m_size; }
+inline size_t sarray_capacity(lean_obj * o) { return to_sarray(o)->m_capacity; }
+inline size_t sarray_byte_size(lean_obj * o) { return sizeof(lean_sarray) + sarray_capacity(o)*sarray_elem_size(o); } // NOLINT
 template<typename T>
-inline void set_sarray_data(lean_obj * o, size_t i, T v) {
-    set_obj_data(o, sizeof(lean_sarray) + sizeof(T)*i, v);
+T * sarray_cptr(lean_obj * o) {
+    lean_assert(is_sarray(o)); lean_assert(sarray_elem_size(o) == sizeof(T));
+    return reinterpret_cast<T*>(reinterpret_cast<char*>(o) + sizeof(lean_sarray));
 }
-
-inline void set_sarray_size(lean_obj * o, size_t sz) {
+template<typename T> T sarray_data(lean_obj * o, size_t i) { return sarray_cptr<T>(o)[i]; }
+template<typename T> void sarray_set_data(lean_obj * o, size_t i, T v) {
+    obj_set_data(o, sizeof(lean_sarray) + sizeof(T)*i, v);
+}
+inline void sarray_set_size(lean_obj * o, size_t sz) {
     lean_assert(is_sarray(o));
     lean_assert(!is_shared(o));
     lean_assert(sz <= sarray_capacity(o));
     to_sarray(o)->m_size = sz;
 }
 
-inline void set_closure_num_fixed(lean_obj * o, unsigned n) {
-    lean_assert(is_closure(o));
-    lean_assert(!is_shared(o));
-    lean_assert(n >= closure_num_fixed(o));
-    lean_assert(n < closure_arity(o));
-    to_closure(o)->m_num_fixed = n;
-}
+/* MPZ */
 
-inline void set_closure_arg(lean_obj * o, unsigned i, lean_obj * a) {
-    lean_assert(i < closure_num_fixed(o));
-    set_obj_data(o, sizeof(lean_closure) + sizeof(lean_obj*)*i, a); // NOLINT
-}
+inline mpz const & mpz_value(lean_obj * o) { return to_mpz(o)->m_value; }
 
 /* String */
 
@@ -524,6 +503,4 @@ inline lean_obj * nat_lxor(lean_obj * a1, lean_obj * a2) {
         return nat_big_xor(a1, a2);
     }
 }
-
-
 }