diff --git a/library/init/lean/ir/extract_cpp.lean b/library/init/lean/ir/extract_cpp.lean
index 130acc0b60..83bbfed573 100644
--- a/library/init/lean/ir/extract_cpp.lean
+++ b/library/init/lean/ir/extract_cpp.lean
@@ -184,33 +184,28 @@ match t with
 | type.object := emit_big_binop x y z big_op
 | _           := emit_infix x y z op
 
-def emit_logical_arith (t : type) (x y z : var) (bool_op : string) (op : string) (big_op : option string) : extract_m unit :=
+def emit_logical_arith (t : type) (x y z : var) (bool_op : string) (op : string) (big_op : string) : extract_m unit :=
 match t with
 | type.bool   := emit_infix x y z bool_op
-| type.object :=
-  (match big_op with
-   | some big_op := emit_big_binop x y z big_op
-   | none        := throw "ill-formed binary operator")
+| type.object := emit_big_binop x y z big_op
 | _           := emit_infix x y z op
 
 def emit_assign_binop (x : var) (t : type) (op : assign_binop) (y z : var) : extract_m unit :=
 match op with
-| assign_binop.add  := emit_arith t x y z "+" "lean::add"
-| assign_binop.sub  := emit_arith t x y z "-" "lean::sub"
-| assign_binop.mul  := emit_arith t x y z "*" "lean::mul"
-| assign_binop.div  := emit_arith t x y z "/" "lean::div"
-| assign_binop.mod  := emit_arith t x y z "%" "lean::mod"
+| assign_binop.add  := emit_arith t x y z "+" "lean::nat_add"
+| assign_binop.sub  := emit_arith t x y z "-" "lean::nat_sub"
+| assign_binop.mul  := emit_arith t x y z "*" "lean::nat_mul"
+| assign_binop.div  := emit_arith t x y z "/" "lean::nat_div"
+| assign_binop.mod  := emit_arith t x y z "%" "lean::nat_mod"
 | assign_binop.shl  := emit_infix x y z "<<"
 | assign_binop.shr  := emit_infix x y z ">>"
-| assign_binop.and  := emit_logical_arith t x y z "&&" "&" (some "lean::and")
-| assign_binop.or   := emit_logical_arith t x y z "||" "|" (some "lean::or")
-| assign_binop.xor  := emit_logical_arith t x y z "!=" "^" none
-| assign_binop.le   := emit_arith t x y z "<=" "lean::le"
-| assign_binop.ge   := emit_arith t x y z ">=" "lean::ge"
-| assign_binop.lt   := emit_arith t x y z "<" "lean::lt"
-| assign_binop.gt   := emit_arith t x y z ">" "lean::gt"
-| assign_binop.eq   := emit_arith t x y z "==" "lean::eq"
-| assign_binop.ne   := emit_arith t x y z "!=" "lean::ne"
+| assign_binop.and  := emit_logical_arith t x y z "&&" "&" "lean::nat_land"
+| assign_binop.or   := emit_logical_arith t x y z "||" "|" "lean::nat_lor"
+| assign_binop.xor  := emit_logical_arith t x y z "!=" "^" "lean::nat_lxor"
+| assign_binop.le   := emit_arith t x y z "<=" "lean::nat_le"
+| assign_binop.lt   := emit_arith t x y z "<"  "lean::nat_lt"
+| assign_binop.eq   := emit_arith t x y z "==" "lean::nat_eq"
+| assign_binop.ne   := emit_arith t x y z "!=" "lean::nat_ne"
 | assign_binop.array_read :=
   (match t with
    | type.object := emit_var x >> emit " = lean::array_obj" >> paren (emit_var y <+> emit_var z)
@@ -234,6 +229,7 @@ def assign_unop2cpp (t : type) : assign_unop → string
 | assign_unop.array_size   := "lean::array_size"
 | assign_unop.sarray_size  := "lean::sarray_size"
 | assign_unop.string_len   := "lean::string_len"
+| assign_unop.succ         := "lean::nat_succ"
 
 def emit_assign_unop (x : var) (t : type) (op : assign_unop) (y : var) : extract_m unit :=
 emit_var x >> emit " = " >> emit (assign_unop2cpp t op) >> paren(emit_var y)
@@ -252,11 +248,10 @@ match l with
 | literal.float v := emit_var x >> emit " = " >> emit v
 | literal.num v   :=
   match t with
-  | type.object := do
-    emit_var x >> emit " = lean::alloc_mpz(lean::mpz(",
-    if v < uint32_sz then emit v >> emit "u"
-    else emit "\"" >> emit v >> emit "\"",
-    emit "))"
+  | type.object :=
+    emit_var x >> emit " = " >>
+    if v < uint32_sz then emit "lean::mk_nat_obj" >> paren(emit v >> emit "u")
+    else emit "lean::mk_mpz_core(lean::mpz(\"" >> emit v >> emit "\"))"
   | _           := emit_var x >> emit " = " >> emit v >> emit_num_suffix t
 
 def unop2cpp : unop → string
diff --git a/library/init/lean/ir/format.lean b/library/init/lean/ir/format.lean
index 2c4b890669..db95435604 100644
--- a/library/init/lean/ir/format.lean
+++ b/library/init/lean/ir/format.lean
@@ -55,7 +55,8 @@ def assign_unop.to_format : assign_unop → format
 | assign_unop.cast          := "cast"
 | assign_unop.array_copy    := "array_copy" | assign_unop.sarray_copy  := "sarray_copy"
 | assign_unop.array_size    := "array_size" | assign_unop.sarray_size  := "sarray_size"
-| assign_unop.string_len    := "string_len"
+| assign_unop.string_len    := "string_len" | assign_unop.succ         := "succ"
+
 
 instance assign_unop.has_to_format : has_to_format assign_unop := ⟨assign_unop.to_format⟩
 instance assign_unop.has_to_string : has_to_string assign_unop := ⟨pretty ∘ to_fmt⟩
@@ -64,8 +65,7 @@ def assign_binop.to_format : assign_binop → format
 | assign_binop.add  := "add"  | assign_binop.sub  := "sub" | assign_binop.mul  := "mul"  | assign_binop.div  := "div"
 | assign_binop.mod  := "mod"  | assign_binop.shl  := "shl" | assign_binop.shr  := "shr"
 | assign_binop.and  := "and"  | assign_binop.or   := "or"  | assign_binop.xor  := "xor"  | assign_binop.le   := "le"
-| assign_binop.ge   := "ge"   | assign_binop.lt   := "lt"  | assign_binop.gt   := "gt"   | assign_binop.eq   := "eq"
-| assign_binop.ne   := "ne"
+| assign_binop.lt   := "lt"   | assign_binop.eq   := "eq"  | assign_binop.ne   := "ne"
 | assign_binop.array_read := "array_read"
 
 instance assign_binop.has_to_format : has_to_format assign_binop := ⟨assign_binop.to_format⟩
diff --git a/library/init/lean/ir/ir.lean b/library/init/lean/ir/ir.lean
index 83dc33e56c..7294d9e8ff 100644
--- a/library/init/lean/ir/ir.lean
+++ b/library/init/lean/ir/ir.lean
@@ -61,15 +61,18 @@ Remark: `sarray_copy` can be used to copy strings.
 - `x : usize := array_size y` stores the size of the array `y : object` into `x`.
 The behavior is unspecified if `y` is not an array of objects.
 
-- `x : usize : sarray_size y` stores the size of the scalar array `y : object` into `x`.
+- `x : usize := sarray_size y` stores the size of the scalar array `y : object` into `x`.
 The behavior is unspecified if `y` is not an array of scalar values.
 
-- `x : usize : string_len y` stores the length of the string `y : object` into `x`.
+- `x : usize := string_len y` stores the length of the string `y : object` into `x`.
 The length is the number of unicode scalar values.
-The behavior is unspecified if `y` is not a string. -/
+The behavior is unspecified if `y` is not a string.
+
+- `x : object := succ y` natural number successor. -/
 inductive assign_unop
 | not | neg | is_scalar | is_shared | is_null | cast | box | unbox
 | array_copy | sarray_copy | array_size | sarray_size | string_len
+| succ
 
 /-- Operators for instructions of the form `x : t := op y z`
 
@@ -102,15 +105,9 @@ Remark: `t ≠ bool`, `t ≠ float`, `t ≠ double` and `t ≠ object`.
 - `x : bool := le y z`: less than or equal to. Remark: `t ≠ bool`.
 If `y` and `z` are `object`, then they must be big numbers.
 
-- `x : bool := ge y z`: greater than or equal to. Remark: `t ≠ bool`.
-If `y` and `z` are `object`, then they must be big numbers.
-
 - `x : bool := lt y z`: less than. Remark: `t ≠ bool`.
 If `y` and `z` are `object`, then they must be big numbers.
 
-- `x : bool := gt y z`: greater than. Remark: `t ≠ bool`.
-If `y` and `z` are `object`, then they must be big numbers.
-
 - `x : bool := eq y z`: equality test. If `y` and `z` are `object`, then they must be big numbers.
 
 - `x : bool := ne y z`: disequality test. If `y` and `z` are `object`, then they must be big numbers.
@@ -119,7 +116,7 @@ If `y` and `z` are `object`, then they must be big numbers.
 If `a` is a scalar array, then `t ≠ object`. If `a` is an (non-scalar) array, then `t = object`. -/
 inductive assign_binop
 | add | sub | mul | div | mod | shl | shr | and | or | xor
-| le  | ge  | lt  | gt  | eq  | ne
+| le  | lt  | eq  | ne
 | array_read -- (scalar) array read
 
 /-- Operators for instructions of the form `op x`
diff --git a/library/init/lean/ir/parser.lean b/library/init/lean/ir/parser.lean
index b5362f1152..d077379b21 100644
--- a/library/init/lean/ir/parser.lean
+++ b/library/init/lean/ir/parser.lean
@@ -46,6 +46,7 @@ def parse_assign_unop : parser assign_unop :=
 <|> (keyword "array_size" >> return assign_unop.array_size)
 <|> (keyword "sarray_size" >> return assign_unop.sarray_size)
 <|> (keyword "string_len" >> return assign_unop.string_len)
+<|> (keyword "succ" >> return assign_unop.succ)
 
 def parse_assign_binop : parser assign_binop :=
     (keyword "add" >> return assign_binop.add)
@@ -59,9 +60,7 @@ def parse_assign_binop : parser assign_binop :=
 <|> (keyword "or" >> return assign_binop.or)
 <|> (keyword "xor" >> return assign_binop.xor)
 <|> (keyword "le" >> return assign_binop.le)
-<|> (keyword "ge" >> return assign_binop.ge)
 <|> (keyword "lt" >> return assign_binop.lt)
-<|> (keyword "gt" >> return assign_binop.gt)
 <|> (keyword "eq" >> return assign_binop.eq)
 <|> (keyword "ne" >> return assign_binop.ne)
 <|> (keyword "array_read" >> return assign_binop.array_read)
diff --git a/library/init/lean/ir/reserved.lean b/library/init/lean/ir/reserved.lean
index f54262b107..46dfb20050 100644
--- a/library/init/lean/ir/reserved.lean
+++ b/library/init/lean/ir/reserved.lean
@@ -17,7 +17,7 @@ def reserved := [ "bool", "byte", "uint16", "uint32", "uint64",
  "apply", "cnstr", "set", "get", "sset", "sget", "array", "read",
  "write", "sarray", "sread", "swrite", "inc", "decs", "dec", "del",
  "phi", "ret", "case", "jmp", "decl", "tt", "ff", "def", "external",
- "defconst"]
+ "defconst", "succ"]
 
 def reserved_set : rbtree string (<) :=
 reserved.foldl rbtree.insert (mk_rbtree string (<))
diff --git a/library/init/lean/ir/type_check.lean b/library/init/lean/ir/type_check.lean
index 13b7b8ea7f..823020fd42 100644
--- a/library/init/lean/ir/type_check.lean
+++ b/library/init/lean/ir/type_check.lean
@@ -56,6 +56,7 @@ match op with
 | assign_unop.array_size    := r = type.usize && t = type.object
 | assign_unop.sarray_size   := r = type.usize && t = type.object
 | assign_unop.string_len    := r = type.usize && t = type.object
+| assign_unop.succ          := r = type.object && t = type.object
 
 /-- Return `tt` iff the instruction `x : r := op y z` is type correct where `y z : t` -/
 def valid_assign_binop_types (op : assign_binop) (r : type) (t₁ t₂ : type) : bool :=
@@ -71,9 +72,7 @@ match op with
 | assign_binop.or   := r = t₁ && r = t₂ && is_bitwise_ty r
 | assign_binop.xor  := r = t₁ && r = t₂ && is_bitwise_ty r
 | assign_binop.le   := r = type.bool && t₁ = t₂ && is_arith_ty t₁
-| assign_binop.ge   := r = type.bool && t₁ = t₂ && is_arith_ty t₁
 | assign_binop.lt   := r = type.bool && t₁ = t₂ && is_arith_ty t₁
-| assign_binop.gt   := r = type.bool && t₁ = t₂ && is_arith_ty t₁
 | assign_binop.eq   := r = type.bool && t₁ = t₂
 | assign_binop.ne   := r = type.bool && t₁ = t₂
 | assign_binop.array_read := t₁ = type.object && t₂ = type.usize
diff --git a/src/runtime/lean_obj.cpp b/src/runtime/lean_obj.cpp
index f18b8c8a36..0203669fb6 100644
--- a/src/runtime/lean_obj.cpp
+++ b/src/runtime/lean_obj.cpp
@@ -107,6 +107,8 @@ void del(lean_obj * o) {
     }
 }
 
+/* Strings */
+
 lean_obj * mk_string(char const * s) {
     size_t sz  = strlen(s);
     size_t len = utf8_strlen(s);
@@ -121,6 +123,132 @@ lean_obj * mk_string(std::string const & s) {
     return mk_string(s.c_str());
 }
 
+/* Natural numbers */
+
+lean_obj * nat_big_add(lean_obj * a1, lean_obj * a2) {
+    lean_assert(!is_scalar(a1) || !is_scalar(a2));
+    if (is_scalar(a1))
+        return mk_mpz_core(unbox(a1) + mpz_value(a2));
+    else if (is_scalar(a2))
+        return mk_mpz_core(mpz_value(a1) + unbox(a2));
+    else
+        return mk_mpz_core(mpz_value(a1) + mpz_value(a2));
+}
+
+lean_obj * nat_big_sub(lean_obj * a1, lean_obj * a2) {
+    lean_assert(!is_scalar(a1) || !is_scalar(a2));
+    if (is_scalar(a1)) {
+        lean_assert(unbox(a1) < mpz_value(a2));
+        return box(0);
+    } else if (is_scalar(a2)) {
+        lean_assert(mpz_value(a1) > unbox(a2));
+        return mk_mpz(mpz_value(a1) - unbox(a2));
+    } else {
+        if (mpz_value(a1) < mpz_value(a2))
+            return box(0);
+        else
+            return mk_mpz(mpz_value(a1) - mpz_value(a2));
+    }
+}
+
+lean_obj * nat_big_mul(lean_obj * a1, lean_obj * a2) {
+    lean_assert(!is_scalar(a1) || !is_scalar(a2));
+    if (is_scalar(a1))
+        return mk_mpz_core(unbox(a1) * mpz_value(a2));
+    else if (is_scalar(a2))
+        return mk_mpz_core(mpz_value(a1) * unbox(a2));
+    else
+        return mk_mpz_core(mpz_value(a1) * mpz_value(a2));
+}
+
+lean_obj * nat_big_div(lean_obj * a1, lean_obj * a2) {
+    lean_assert(!is_scalar(a1) || !is_scalar(a2));
+    if (is_scalar(a1)) {
+        lean_assert(mpz_value(a2) != 0);
+        lean_assert(unbox(a1) / mpz_value(a2) == 0);
+        return box(0);
+    } else if (is_scalar(a2)) {
+        unsigned n2 = unbox(a2);
+        return n2 == 0 ? a2 : mk_mpz(mpz_value(a1) / n2);
+    } else {
+        lean_assert(mpz_value(a2) != 0);
+        return mk_mpz(mpz_value(a1) / mpz_value(a2));
+    }
+}
+
+lean_obj * nat_big_mod(lean_obj * a1, lean_obj * a2) {
+    lean_assert(!is_scalar(a1) || !is_scalar(a2));
+    if (is_scalar(a1)) {
+        lean_assert(mpz_value(a2) != 0);
+        return a1;
+    } else if (is_scalar(a2)) {
+        unsigned n2 = unbox(a2);
+        return n2 == 0 ? a2 : box((mpz_value(a1) % mpz(n2)).get_unsigned_int());
+    } else {
+        lean_assert(mpz_value(a2) != 0);
+        return mk_mpz(mpz_value(a1) % mpz_value(a2));
+    }
+}
+
+bool nat_big_eq(lean_obj * a1, lean_obj * a2) {
+    if (is_scalar(a1))
+        return unbox(a1) == mpz_value(a2);
+    else if (is_scalar(a2))
+        return mpz_value(a1) == unbox(a2);
+    else
+        return mpz_value(a1) == mpz_value(a2);
+}
+
+bool nat_big_le(lean_obj * a1, lean_obj * a2) {
+    if (is_scalar(a1))
+        return unbox(a1) <= mpz_value(a2);
+    else if (is_scalar(a2))
+        return mpz_value(a1) <= unbox(a2);
+    else
+        return mpz_value(a1) <= mpz_value(a2);
+}
+
+bool nat_big_lt(lean_obj * a1, lean_obj * a2) {
+    if (is_scalar(a1))
+        return unbox(a1) < mpz_value(a2);
+    else if (is_scalar(a2))
+        return mpz_value(a1) < unbox(a2);
+    else
+        return mpz_value(a1) < mpz_value(a2);
+}
+
+lean_obj * nat_big_land(lean_obj * a1, lean_obj * a2) {
+    lean_assert(!is_scalar(a1) || !is_scalar(a2));
+    if (is_scalar(a1))
+        return mk_mpz(mpz(unbox(a1)) & mpz_value(a2));
+    else if (is_scalar(a2))
+        return mk_mpz(mpz_value(a1) & mpz(unbox(a2)));
+    else
+        return mk_mpz(mpz_value(a1) & mpz_value(a2));
+}
+
+lean_obj * nat_big_lor(lean_obj * a1, lean_obj * a2) {
+    lean_assert(!is_scalar(a1) || !is_scalar(a2));
+    if (is_scalar(a1))
+        return mk_mpz(mpz(unbox(a1)) | mpz_value(a2));
+    else if (is_scalar(a2))
+        return mk_mpz(mpz_value(a1) | mpz(unbox(a2)));
+    else
+        return mk_mpz(mpz_value(a1) | mpz_value(a2));
+}
+
+lean_obj * nat_big_lxor(lean_obj * a1, lean_obj * a2) {
+    lean_assert(!is_scalar(a1) || !is_scalar(a2));
+    if (is_scalar(a1))
+        return mk_mpz(mpz(unbox(a1)) ^ mpz_value(a2));
+    else if (is_scalar(a2))
+        return mk_mpz(mpz_value(a1) ^ mpz(unbox(a2)));
+    else
+        return mk_mpz(mpz_value(a1) ^ mpz_value(a2));
+}
+
+/* Debugging helper functions */
+
 void dbg_print_str(lean_obj * o) {
     lean_assert(is_string(o));
     std::cout << c_str(o) << "\n";
diff --git a/src/runtime/lean_obj.h b/src/runtime/lean_obj.h
index 48c67ff22f..39a692da27 100644
--- a/src/runtime/lean_obj.h
+++ b/src/runtime/lean_obj.h
@@ -6,7 +6,9 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <string>
+#include "runtime/compiler_hints.h"
 #include "runtime/mpz.h"
+#include "runtime/int64.h"
 
 namespace lean {
 enum class lean_obj_kind { Constructor, Closure, Array, ScalarArray, MPZ, External };
@@ -93,7 +95,7 @@ struct lean_external : public lean_obj {
 };
 
 inline bool is_scalar(lean_obj * o) { return (reinterpret_cast<uintptr_t>(o) & 1) == 1; }
-inline lean_obj * box(unsigned n) { return reinterpret_cast<lean_obj*>(static_cast<uintptr_t>((n << 1) | 1)); }
+inline lean_obj * box(unsigned n) { return reinterpret_cast<lean_obj*>((static_cast<uintptr_t>(n) << 1) | 1); }
 inline unsigned unbox(lean_obj * o) { return reinterpret_cast<uintptr_t>(o) >> 1; }
 
 /* Generic Lean object delete operation.
@@ -316,12 +318,188 @@ inline void set_closure_arg(lean_obj * o, unsigned i, lean_obj * a) {
     set_obj_data(o, sizeof(lean_closure) + sizeof(lean_obj*)*i, a); // NOLINT
 }
 
-/* Constructors */
-
-inline lean_obj * mk_mpz(mpz const & m) { return alloc_mpz(m); }
+/* String */
 
 lean_obj * mk_string(char const * s);
 lean_obj * mk_string(std::string const & s);
 inline bool is_string(lean_obj * o) { return !is_scalar(o) && is_sarray(o) && sarray_elem_size(o) == 1; }
 inline char const * c_str(lean_obj * o) { lean_assert(is_string(o)); return sarray_cptr<char>(o) + sizeof(size_t); }
+
+/* Natural numbers */
+
+#define LEAN_MAX_SMALL_NAT (sizeof(void*) == 8 ? std::numeric_limits<unsigned>::max() : (std::numeric_limits<unsigned>::max() >> 1)) // NOLINT
+
+inline lean_obj * mk_mpz_core(mpz const & m) {
+    lean_assert(m > LEAN_MAX_SMALL_NAT);
+    return alloc_mpz(m);
+}
+
+inline lean_obj * mk_mpz(mpz const & m) {
+    if (m > LEAN_MAX_SMALL_NAT)
+        return mk_mpz_core(m);
+    else
+        return box(m.get_unsigned_int());
+}
+
+inline lean_obj * mk_nat_obj(unsigned n) {
+    if (sizeof(void*) == 8) { // NOLINT
+        return box(n);
+    } else if (n <= LEAN_MAX_SMALL_NAT) {
+        return box(n);
+    } else {
+        return mk_mpz_core(mpz(n));
+    }
+}
+
+inline lean_obj * mk_nat_obj(uint64 n) {
+    if (LEAN_LIKELY(n < LEAN_MAX_SMALL_NAT)) {
+        return box(n);
+    } else {
+        return mk_mpz_core(mpz(n));
+    }
+}
+
+inline uint64 nat2uint64(lean_obj * a) {
+    lean_assert(is_scalar(a));
+    return unbox(a);
+}
+
+inline lean_obj * nat_succ(lean_obj * a) {
+    if (LEAN_LIKELY(is_scalar(a))) {
+        return mk_nat_obj(nat2uint64(a) + 1);
+    } else {
+        return mk_mpz_core(mpz_value(a) + 1);
+    }
+}
+
+lean_obj * nat_big_add(lean_obj * a1, lean_obj * a2);
+
+inline lean_obj * nat_add(lean_obj * a1, lean_obj * a2) {
+    if (LEAN_LIKELY(is_scalar(a1) && is_scalar(a2))) {
+        return mk_nat_obj(nat2uint64(a1) + nat2uint64(a2));
+    } else {
+        return nat_big_add(a1, a2);
+    }
+}
+
+lean_obj * nat_big_sub(lean_obj * a1, lean_obj * a2);
+
+inline lean_obj * nat_sub(lean_obj * a1, lean_obj * a2) {
+    if (LEAN_LIKELY(is_scalar(a1) && is_scalar(a2))) {
+        unsigned n1 = unbox(a1);
+        unsigned n2 = unbox(a2);
+        if (n1 < n2)
+            return box(0);
+        else
+            return box(n1 - n2);
+    } else {
+        return nat_big_sub(a1, a2);
+    }
+}
+
+lean_obj * nat_big_mul(lean_obj * a1, lean_obj * a2);
+
+inline lean_obj * nat_mul(lean_obj * a1, lean_obj * a2) {
+    if (LEAN_LIKELY(is_scalar(a1) && is_scalar(a2))) {
+        return mk_nat_obj(nat2uint64(a1) * nat2uint64(a2));
+    } else {
+        return nat_big_mul(a1, a2);
+    }
+}
+
+lean_obj * nat_big_div(lean_obj * a1, lean_obj * a2);
+
+inline lean_obj * nat_div(lean_obj * a1, lean_obj * a2) {
+    if (LEAN_LIKELY(is_scalar(a1) && is_scalar(a2))) {
+        unsigned n1 = unbox(a1);
+        unsigned n2 = unbox(a2);
+        if (n2 == 0)
+            return box(0);
+        else
+            return box(n1 / n2);
+    } else {
+        return nat_big_div(a1, a2);
+    }
+}
+
+lean_obj * nat_big_mod(lean_obj * a1, lean_obj * a2);
+
+inline lean_obj * nat_mod(lean_obj * a1, lean_obj * a2) {
+    if (LEAN_LIKELY(is_scalar(a1) && is_scalar(a2))) {
+        unsigned n1 = unbox(a1);
+        unsigned n2 = unbox(a2);
+        if (n2 == 0)
+            return box(0);
+        else
+            return box(n1 % n2);
+    } else {
+        return nat_big_mod(a1, a2);
+    }
+}
+
+bool nat_big_eq(lean_obj * a1, lean_obj * a2);
+
+inline bool nat_eq(lean_obj * a1, lean_obj * a2) {
+    if (LEAN_LIKELY(is_scalar(a1) && is_scalar(a2))) {
+        return a1 == a2;
+    } else {
+        return nat_big_eq(a1, a2);
+    }
+}
+
+inline bool nat_ne(lean_obj * a1, lean_obj * a2) {
+    return !nat_eq(a1, a2);
+}
+
+bool nat_big_le(lean_obj * a1, lean_obj * a2);
+
+inline bool nat_le(lean_obj * a1, lean_obj * a2) {
+    if (LEAN_LIKELY(is_scalar(a1) && is_scalar(a2))) {
+        return a1 <= a2;
+    } else {
+        return nat_big_le(a1, a2);
+    }
+}
+
+bool nat_big_lt(lean_obj * a1, lean_obj * a2);
+
+inline bool nat_lt(lean_obj * a1, lean_obj * a2) {
+    if (LEAN_LIKELY(is_scalar(a1) && is_scalar(a2))) {
+        return a1 < a2;
+    } else {
+        return nat_big_lt(a1, a2);
+    }
+}
+
+lean_obj * nat_big_land(lean_obj * a1, lean_obj * a2);
+
+inline lean_obj * nat_land(lean_obj * a1, lean_obj * a2) {
+    if (LEAN_LIKELY(is_scalar(a1) && is_scalar(a2))) {
+        return reinterpret_cast<lean_obj*>(reinterpret_cast<uintptr_t>(a1) & reinterpret_cast<uintptr_t>(a2));
+    } else {
+        return nat_big_land(a1, a2);
+    }
+}
+
+lean_obj * nat_big_lor(lean_obj * a1, lean_obj * a2);
+
+inline lean_obj * nat_lor(lean_obj * a1, lean_obj * a2) {
+    if (LEAN_LIKELY(is_scalar(a1) && is_scalar(a2))) {
+        return reinterpret_cast<lean_obj*>(reinterpret_cast<uintptr_t>(a1) | reinterpret_cast<uintptr_t>(a2));
+    } else {
+        return nat_big_lor(a1, a2);
+    }
+}
+
+lean_obj * nat_big_xor(lean_obj * a1, lean_obj * a2);
+
+inline lean_obj * nat_lxor(lean_obj * a1, lean_obj * a2) {
+    if (LEAN_LIKELY(is_scalar(a1) && is_scalar(a2))) {
+        return box(unbox(a1) ^ unbox(a2));
+    } else {
+        return nat_big_xor(a1, a2);
+    }
+}
+
+
 }
diff --git a/tests/ir/tst2.ir b/tests/ir/tst2.ir
new file mode 100644
index 0000000000..43c4861330
--- /dev/null
+++ b/tests/ir/tst2.ir
@@ -0,0 +1,32 @@
+[lean_dbg_print_str] external print_str (s : object)
+[lean_dbg_print_num] external print_num (s : object)
+
+def print_bool (b : bool) :=
+entry:
+  case b [false_lbl, true_lbl];
+true_lbl:
+  s1 : object := "true";
+  call print_str s1;
+  ret;
+false_lbl:
+  s2 : object := "false";
+  call print_str s2;
+  ret;
+
+def main : int32 :=
+entry:
+  n1 : object := 10;
+  n2 : object := 20;
+  n3 : object := add n1 n2;
+  n4 : object := mul n3 n3;
+  call print_num n4;
+  c1 : bool := lt n4 n1;
+  call print_bool c1;
+  c2 : bool := le n4 n4;
+  call print_bool c2;
+  n5 : object := 100000000000000000;
+  n6 : object := 200000000000000000;
+  n7 : object := add n5 n6;
+  call print_num n7;
+  r : int32 := 0;
+  ret r;
\ No newline at end of file