diff --git a/library/init/core.lean b/library/init/core.lean
index 9b36d31d09..58a840b5e1 100644
--- a/library/init/core.lean
+++ b/library/init/core.lean
@@ -427,7 +427,8 @@ export has_insert (insert)
 has_insert.insert a ∅
 
 /- nat basic instances -/
-protected def nat.add : nat → nat → nat
+@[extern cpp "lean::nat_add"]
+protected def nat.add : (@& nat) → (@& nat) → nat
 | a  nat.zero     := a
 | a  (nat.succ b) := nat.succ (nat.add a b)
 
diff --git a/library/init/data/nat/basic.lean b/library/init/data/nat/basic.lean
index 7081b370a0..c8dc3ad6ed 100644
--- a/library/init/data/nat/basic.lean
+++ b/library/init/data/nat/basic.lean
@@ -10,6 +10,7 @@ notation `ℕ` := nat
 
 namespace nat
 
+@[extern cpp "lean::nat_dec_eq"]
 def beq : nat → nat → bool
 | zero     zero     := tt
 | zero     (succ m) := ff
@@ -34,13 +35,15 @@ theorem ne_of_beq_eq_ff : ∀ {n m : nat}, beq n m = ff → n ≠ m
   have n ≠ m, from ne_of_beq_eq_ff this,
   nat.no_confusion h₂ (λ h₂, absurd h₂ this)
 
-protected def dec_eq (n m : nat) : decidable (n = m) :=
+@[extern cpp "lean::nat_dec_eq"]
+protected def dec_eq (n m : @& nat) : decidable (n = m) :=
 if h : beq n m = tt then is_true (eq_of_beq_eq_tt h)
 else is_false (ne_of_beq_eq_ff (eq_ff_of_ne_tt h))
 
 @[inline] instance : decidable_eq nat :=
 {dec_eq := nat.dec_eq}
 
+@[extern cpp "lean::nat_dec_le"]
 def ble : nat → nat → bool
 | zero     zero     := tt
 | zero     (succ m) := tt
@@ -59,15 +62,18 @@ nat.le (succ n) m
 instance : has_lt nat :=
 ⟨nat.lt⟩
 
+@[extern cpp inline "lean::nat_sub(#1, lean::box(1))"]
 def pred : nat → nat
 | 0     := 0
 | (a+1) := a
 
-protected def sub : nat → nat → nat
+@[extern cpp "lean::nat_sub"]
+protected def sub : (@& nat) → (@& nat) → nat
 | a 0     := a
 | a (b+1) := pred (sub a b)
 
-protected def mul : nat → nat → nat
+@[extern cpp "lean::nat_mul"]
+protected def mul : (@& nat) → (@& nat) → nat
 | a 0     := 0
 | a (b+1) := (mul a b) + a
 
@@ -252,10 +258,12 @@ theorem pred_le_pred : ∀ {n m : nat}, n ≤ m → pred n ≤ pred m
 theorem le_of_succ_le_succ {n m : nat} : succ n ≤ succ m → n ≤ m :=
 pred_le_pred
 
-instance dec_le (n m : nat) : decidable (n ≤ m) :=
+@[extern cpp "lean::nat_dec_le"]
+instance dec_le (n m : @& nat) : decidable (n ≤ m) :=
 dec_eq (ble n m) tt
 
-instance dec_lt (n m : nat) : decidable (n < m) :=
+@[extern cpp "lean::nat_dec_lt"]
+instance dec_lt (n m : @& nat) : decidable (n < m) :=
 nat.dec_le (succ n) m
 
 protected theorem eq_or_lt_of_le : ∀ {n m: nat}, n ≤ m → n = m ∨ n < m
diff --git a/library/init/data/nat/div.lean b/library/init/data/nat/div.lean
index 26b21f6b4a..7c3bc21485 100644
--- a/library/init/data/nat/div.lean
+++ b/library/init/data/nat/div.lean
@@ -13,7 +13,9 @@ private def div_rec_lemma {x y : nat} : 0 < y ∧ y ≤ x → x - y < x :=
 private def div.F (x : nat) (f : Π x₁, x₁ < x → nat → nat) (y : nat) : nat :=
 if h : 0 < y ∧ y ≤ x then f (x - y) (div_rec_lemma h) y + 1 else zero
 
-protected def div := well_founded.fix lt_wf div.F
+@[extern cpp "lean::nat_div"]
+protected def div (a b : @& nat) : nat :=
+well_founded.fix lt_wf div.F a b
 
 instance : has_div nat :=
 ⟨nat.div⟩
@@ -43,7 +45,9 @@ well_founded.fix nat.lt_wf (div.induction.F C h₁ h₂) x y
 private def mod.F (x : nat) (f : Π x₁, x₁ < x → nat → nat) (y : nat) : nat :=
 if h : 0 < y ∧ y ≤ x then f (x - y) (div_rec_lemma h) y else x
 
-protected def mod := well_founded.fix lt_wf mod.F
+@[extern cpp "lean::nat_mod"]
+protected def mod (a b : @& nat) : nat :=
+well_founded.fix lt_wf mod.F a b
 
 instance : has_mod nat :=
 ⟨nat.mod⟩
diff --git a/src/library/compiler/builtin.cpp b/src/library/compiler/builtin.cpp
index c69eb130df..c61af8f24f 100644
--- a/src/library/compiler/builtin.cpp
+++ b/src/library/compiler/builtin.cpp
@@ -146,84 +146,6 @@ bool get_native_borrowed_info(environment const & env, name const & c, buffer<bo
 
 void initialize_builtin() {
     g_initial_native_decls = new native_decl_map();
-
-    expr o           = mk_enf_object_type();
-    expr u8          = mk_constant(get_uint8_name());
-    expr u16         = mk_constant(get_uint16_name());
-    expr u32         = mk_constant(get_uint32_name());
-    expr u64         = mk_constant(get_uint64_name());
-    expr us          = mk_constant(get_usize_name());
-    expr o_o         = mk_arrow(o, o);
-    expr o_o_o       = mk_arrow(o, o_o);
-    expr o_o_o_o     = mk_arrow(o, o_o_o);
-    expr o_o_o_o_o   = mk_arrow(o, o_o_o_o);
-
-    expr o_u8        = mk_arrow(o, u8);
-    expr o_u8_u8_o_o = mk_arrow(o, mk_arrow(u8, mk_arrow(u8, o_o)));
-    expr u8_u8       = mk_arrow(u8, u8);
-    expr u8_u8_u8    = mk_arrow(u8, u8_u8);
-    expr u8_o_u8     = mk_arrow(u8, o_u8);
-    expr u8_o        = mk_arrow(u8, o);
-    expr u8_u8_o     = mk_arrow(u8, u8_o);
-    expr o_o_u8      = mk_arrow(o, o_u8);
-
-    expr o_u16         = mk_arrow(o, u16);
-    expr o_u16_u16_o_o = mk_arrow(o, mk_arrow(u16, mk_arrow(u16, o_o)));
-    expr u16_u16       = mk_arrow(u16, u16);
-    expr u16_u16_u16   = mk_arrow(u16, u16_u16);
-    expr u16_o_u16     = mk_arrow(u16, o_u16);
-    expr u16_o         = mk_arrow(u16, o);
-    expr u16_u16_o     = mk_arrow(u16, u16_o);
-    expr u16_u16_u8    = mk_arrow(u16, mk_arrow(u16, u8));
-
-    expr o_u32         = mk_arrow(o, u32);
-    expr o_u32_o       = mk_arrow(o, mk_arrow(u32, o));
-    expr o_u32_u32_o_o = mk_arrow(o, mk_arrow(u32, mk_arrow(u32, o_o)));
-    expr u32_u32       = mk_arrow(u32, u32);
-    expr u32_u32_u32   = mk_arrow(u32, u32_u32);
-    expr u32_o_u32     = mk_arrow(u32, o_u32);
-    expr u32_o         = mk_arrow(u32, o);
-    expr u32_u32_o     = mk_arrow(u32, u32_o);
-    expr u32_u32_u8    = mk_arrow(u32, mk_arrow(u32, u8));
-
-    expr o_u64         = mk_arrow(o, u64);
-    expr o_u64_u64_o_o = mk_arrow(o, mk_arrow(u64, mk_arrow(u64, o_o)));
-    expr u64_u64       = mk_arrow(u64, u64);
-    expr u64_u64_u64   = mk_arrow(u64, u64_u64);
-    expr u64_o_u64     = mk_arrow(u64, o_u64);
-    expr u64_o         = mk_arrow(u64, o);
-    expr u64_u64_o     = mk_arrow(u64, u64_o);
-    expr u64_u64_u8    = mk_arrow(u64, mk_arrow(u64, u8));
-
-    expr o_us          = mk_arrow(o, us);
-    expr o_us_us_o_o   = mk_arrow(o, mk_arrow(us, mk_arrow(us, o_o)));
-    expr us_us         = mk_arrow(us, us);
-    expr us_us_us      = mk_arrow(us, us_us);
-    expr us_o_us       = mk_arrow(us, o_us);
-    expr us_o          = mk_arrow(us, o);
-    expr us_us_o       = mk_arrow(us, us_o);
-    expr us_us_u8      = mk_arrow(us, mk_arrow(us, u8));
-
-    list<bool> b{true};
-    list<bool> bb{true, true};
-    list<bool> c{false};
-    list<bool> cc{false, false};
-    list<bool> cb{false, true};
-    list<bool> bc{true, false};
-    list<bool> bbb{true, true, true};
-    list<bool> bccc{true, false, false, false};
-    list<bool> bbcc{true, true, false, false};
-
-    /* nat builtin functions */
-    register_builtin(name({"nat", "add"}), o_o_o, "lean::nat_add", bb);
-    register_builtin(name({"nat", "sub"}), o_o_o, "lean::nat_sub", bb);
-    register_builtin(name({"nat", "mul"}), o_o_o, "lean::nat_mul", bb);
-    register_builtin(name({"nat", "div"}), o_o_o, "lean::nat_div", bb);
-    register_builtin(name({"nat", "mod"}), o_o_o, "lean::nat_mod", bb);
-    register_builtin(name({"nat", "dec_eq"}), o_o_u8, "lean::nat_dec_eq", bb);
-    register_builtin(name({"nat", "dec_lt"}), o_o_u8, "lean::nat_dec_lt", bb);
-    register_builtin(name({"nat", "dec_le"}), o_o_u8, "lean::nat_dec_le", bb);
-
     g_ext = new native_decls_reg();
 }
 
diff --git a/src/library/vm/vm_nat.cpp b/src/library/vm/vm_nat.cpp
index 5f0fec3bf0..04a322f67f 100644
--- a/src/library/vm/vm_nat.cpp
+++ b/src/library/vm/vm_nat.cpp
@@ -127,6 +127,10 @@ vm_obj nat_sub(vm_obj const & a1, vm_obj const & a2) {
     }
 }
 
+vm_obj nat_pred(vm_obj const & a) {
+    return nat_sub(a, mk_vm_simple(1));
+}
+
 vm_obj nat_div(vm_obj const & a1, vm_obj const & a2) {
     if (LEAN_LIKELY(is_simple(a1) && is_simple(a2))) {
         unsigned v1 = cidx(a1);
@@ -191,6 +195,7 @@ void initialize_vm_nat() {
     DECLARE_VM_BUILTIN(name({"nat", "add"}),        nat_add);
     DECLARE_VM_BUILTIN(name({"nat", "mul"}),        nat_mul);
     DECLARE_VM_BUILTIN(name({"nat", "sub"}),        nat_sub);
+    DECLARE_VM_BUILTIN(name({"nat", "pred"}),       nat_pred);
     DECLARE_VM_BUILTIN(name({"nat", "div"}),        nat_div);
     DECLARE_VM_BUILTIN(name({"nat", "mod"}),        nat_mod);
     DECLARE_VM_BUILTIN(name({"nat", "dec_eq"}),     nat_decidable_eq);