diff --git a/library/debugger/util.lean b/library/debugger/util.lean
index 6b5f0c5642..3188032781 100644
--- a/library/debugger/util.lean
+++ b/library/debugger/util.lean
@@ -79,19 +79,20 @@ meta def type_to_string : option expr → nat → vm string
 | none i := do
   o ← vm.stack_obj i,
   match o^.kind with
-  | vm_obj_kind.simple       := return "[tagged value]"
-  | vm_obj_kind.constructor  := return "[constructor]"
-  | vm_obj_kind.closure      := return "[closure]"
-  | vm_obj_kind.mpz          := return "[big num]"
-  | vm_obj_kind.name         := return "name"
-  | vm_obj_kind.level        := return "level"
-  | vm_obj_kind.expr         := return "expr"
-  | vm_obj_kind.declaration  := return "declaration"
-  | vm_obj_kind.environment  := return "environment"
-  | vm_obj_kind.tactic_state := return "tactic_state"
-  | vm_obj_kind.format       := return "format"
-  | vm_obj_kind.options      := return "options"
-  | vm_obj_kind.other        := return "[other]"
+  | vm_obj_kind.simple         := return "[tagged value]"
+  | vm_obj_kind.constructor    := return "[constructor]"
+  | vm_obj_kind.closure        := return "[closure]"
+  | vm_obj_kind.native_closure := return "[native closure]"
+  | vm_obj_kind.mpz            := return "[big num]"
+  | vm_obj_kind.name           := return "name"
+  | vm_obj_kind.level          := return "level"
+  | vm_obj_kind.expr           := return "expr"
+  | vm_obj_kind.declaration    := return "declaration"
+  | vm_obj_kind.environment    := return "environment"
+  | vm_obj_kind.tactic_state   := return "tactic_state"
+  | vm_obj_kind.format         := return "format"
+  | vm_obj_kind.options        := return "options"
+  | vm_obj_kind.other          := return "[other]"
   end
 | (some type) i := do
   fmt ← vm.pp_expr type,
diff --git a/library/init/meta/vm.lean b/library/init/meta/vm.lean
index a334321ef3..908ab08085 100644
--- a/library/init/meta/vm.lean
+++ b/library/init/meta/vm.lean
@@ -9,7 +9,7 @@ import init.meta.tactic init.data.option.basic
 meta constant vm_obj : Type
 
 inductive vm_obj_kind
-| simple | constructor | closure | mpz
+| simple | constructor | closure | native_closure | mpz
 | name | level | expr | declaration
 | environment | tactic_state | format
 | options | other
diff --git a/src/library/tactic/vm_monitor.cpp b/src/library/tactic/vm_monitor.cpp
index 3e005cf747..525c00c3fe 100644
--- a/src/library/tactic/vm_monitor.cpp
+++ b/src/library/tactic/vm_monitor.cpp
@@ -61,17 +61,18 @@ vm_obj _vm_obj_kind(vm_obj const & o) {
     case vm_obj_kind::Simple: return mk_vm_simple(0);
     case vm_obj_kind::Constructor: return mk_vm_simple(1);
     case vm_obj_kind::Closure: return mk_vm_simple(2);
-    case vm_obj_kind::MPZ: return mk_vm_simple(3);
+    case vm_obj_kind::NativeClosure: return mk_vm_simple(3);
+    case vm_obj_kind::MPZ: return mk_vm_simple(4);
     case vm_obj_kind::External:
-        if (is_name(o)) return mk_vm_simple(4);
-        else if (is_level(o)) return mk_vm_simple(5);
-        else if (is_expr(o)) return mk_vm_simple(6);
-        else if (is_declaration(o)) return mk_vm_simple(7);
-        else if (is_env(o)) return mk_vm_simple(8);
-        else if (is_tactic_state(o)) return mk_vm_simple(9);
-        else if (is_format(o)) return mk_vm_simple(10);
-        else if (is_options(o)) return mk_vm_simple(11);
-        else return mk_vm_simple(12);
+        if (is_name(o)) return mk_vm_simple(5);
+        else if (is_level(o)) return mk_vm_simple(6);
+        else if (is_expr(o)) return mk_vm_simple(7);
+        else if (is_declaration(o)) return mk_vm_simple(8);
+        else if (is_env(o)) return mk_vm_simple(9);
+        else if (is_tactic_state(o)) return mk_vm_simple(10);
+        else if (is_format(o)) return mk_vm_simple(11);
+        else if (is_options(o)) return mk_vm_simple(12);
+        else return mk_vm_simple(13);
     }
     lean_unreachable();
 }
diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp
index 014186ccc8..6b25abed49 100644
--- a/src/library/vm/vm.cpp
+++ b/src/library/vm/vm.cpp
@@ -101,14 +101,6 @@ vm_obj mk_vm_constructor(unsigned cidx, vm_obj const & o1, vm_obj const & o2, vm
     return mk_vm_constructor(cidx, 4, args);
 }
 
-vm_obj mk_native_closure(environment const & env, name const & n, std::initializer_list<vm_obj const> args) {
-    return mk_native_closure(env, n, args.size(), args.begin());
-}
-
-vm_obj mk_native_closure(environment const & /* env */, name const & n, unsigned /* sz */, vm_obj const * /* data */) {
-    return get_vm_state().get_constant(n);
-}
-
 vm_obj mk_vm_closure(unsigned fn_idx, unsigned sz, vm_obj const * data) {
     return mk_vm_composite(vm_obj_kind::Closure, fn_idx, sz, data);
 }
@@ -150,6 +142,113 @@ void vm_mpz::dealloc() {
     get_small_allocator().deallocate(sizeof(vm_mpz), this);
 }
 
+/* TODO(Leo, Jared): delete mk_native_closure that takes environment as argument */
+vm_obj mk_native_closure(environment const & env, name const & n, std::initializer_list<vm_obj const> args) {
+    return mk_native_closure(env, n, args.size(), args.begin());
+}
+
+vm_obj mk_native_closure(environment const & /* env */, name const & n, unsigned /* sz */, vm_obj const * /* data */) {
+    return get_vm_state().get_constant(n);
+}
+
+vm_native_closure::vm_native_closure(vm_cfunction fn, unsigned arity, unsigned num_args, vm_obj const * args):
+    vm_obj_cell(vm_obj_kind::NativeClosure), m_fn(fn), m_arity(arity), m_num_args(num_args) {
+    /* If the following assertion fails, then it is not necessary to create a closure */
+    lean_assert(arity > num_args);
+    vm_obj * new_args = get_args_ptr();
+    std::uninitialized_copy(args, args + num_args, new_args);
+}
+
+void vm_native_closure::dealloc(buffer<vm_obj_cell*> & todelete) {
+    vm_obj * args  = get_args_ptr();
+    unsigned nargs = m_num_args;
+    for (unsigned i = 0; i < nargs; i++) {
+        dec_ref(args[i], todelete);
+    }
+    this->~vm_native_closure();
+    get_small_allocator().deallocate(sizeof(vm_native_closure) + nargs * sizeof(vm_obj), this);
+}
+
+vm_obj mk_native_closure(vm_cfunction fn, unsigned arity, unsigned num_args, vm_obj const * args) {
+    return vm_obj(new (get_small_allocator().allocate(sizeof(vm_native_closure) + num_args * sizeof(vm_obj))) vm_native_closure(fn, arity, num_args, args));
+}
+
+vm_obj mk_native_closure(vm_cfunction fn, unsigned arity, std::initializer_list<vm_obj> const & args) {
+    return mk_native_closure(fn, arity, args.size(), args.begin());
+}
+
+vm_obj mk_native_closure(vm_cfunction_1 fn, unsigned num_args, vm_obj const * args) {
+    return mk_native_closure(reinterpret_cast<vm_cfunction>(fn), 1, num_args, args);
+}
+
+vm_obj mk_native_closure(vm_cfunction_2 fn, unsigned num_args, vm_obj const * args) {
+    return mk_native_closure(reinterpret_cast<vm_cfunction>(fn), 2, num_args, args);
+}
+
+vm_obj mk_native_closure(vm_cfunction_3 fn, unsigned num_args, vm_obj const * args) {
+    return mk_native_closure(reinterpret_cast<vm_cfunction>(fn), 3, num_args, args);
+}
+
+vm_obj mk_native_closure(vm_cfunction_4 fn, unsigned num_args, vm_obj const * args) {
+    return mk_native_closure(reinterpret_cast<vm_cfunction>(fn), 4, num_args, args);
+}
+
+vm_obj mk_native_closure(vm_cfunction_5 fn, unsigned num_args, vm_obj const * args) {
+    return mk_native_closure(reinterpret_cast<vm_cfunction>(fn), 5, num_args, args);
+}
+
+vm_obj mk_native_closure(vm_cfunction_6 fn, unsigned num_args, vm_obj const * args) {
+    return mk_native_closure(reinterpret_cast<vm_cfunction>(fn), 6, num_args, args);
+}
+
+vm_obj mk_native_closure(vm_cfunction_7 fn, unsigned num_args, vm_obj const * args) {
+    return mk_native_closure(reinterpret_cast<vm_cfunction>(fn), 7, num_args, args);
+}
+
+vm_obj mk_native_closure(vm_cfunction_8 fn, unsigned num_args, vm_obj const * args) {
+    return mk_native_closure(reinterpret_cast<vm_cfunction>(fn), 8, num_args, args);
+}
+
+vm_obj mk_native_closure(vm_cfunction_N fn, unsigned arity, unsigned num_args, vm_obj const * args) {
+    return mk_native_closure(reinterpret_cast<vm_cfunction>(fn), arity, num_args, args);
+}
+
+vm_obj mk_native_closure(vm_cfunction_1 fn, std::initializer_list<vm_obj> const & args) {
+    return mk_native_closure(fn, args.size(), args.begin());
+}
+
+vm_obj mk_native_closure(vm_cfunction_2 fn, std::initializer_list<vm_obj> const & args) {
+    return mk_native_closure(fn, args.size(), args.begin());
+}
+
+vm_obj mk_native_closure(vm_cfunction_3 fn, std::initializer_list<vm_obj> const & args) {
+    return mk_native_closure(fn, args.size(), args.begin());
+}
+
+vm_obj mk_native_closure(vm_cfunction_4 fn, std::initializer_list<vm_obj> const & args) {
+    return mk_native_closure(fn, args.size(), args.begin());
+}
+
+vm_obj mk_native_closure(vm_cfunction_5 fn, std::initializer_list<vm_obj> const & args) {
+    return mk_native_closure(fn, args.size(), args.begin());
+}
+
+vm_obj mk_native_closure(vm_cfunction_6 fn, std::initializer_list<vm_obj> const & args) {
+    return mk_native_closure(fn, args.size(), args.begin());
+}
+
+vm_obj mk_native_closure(vm_cfunction_7 fn, std::initializer_list<vm_obj> const & args) {
+    return mk_native_closure(fn, args.size(), args.begin());
+}
+
+vm_obj mk_native_closure(vm_cfunction_8 fn, std::initializer_list<vm_obj> const & args) {
+    return mk_native_closure(fn, args.size(), args.begin());
+}
+
+vm_obj mk_native_closure(vm_cfunction_N fn, unsigned arity, std::initializer_list<vm_obj> const & args) {
+    return mk_native_closure(fn, arity, args.size(), args.begin());
+}
+
 void vm_obj_cell::dealloc() {
     try {
         buffer<vm_obj_cell*> todo;
@@ -159,11 +258,12 @@ void vm_obj_cell::dealloc() {
             todo.pop_back();
             lean_assert(it->get_rc() == 0);
             switch (it->kind()) {
-            case vm_obj_kind::Simple:      lean_unreachable();
-            case vm_obj_kind::Constructor: to_composite(it)->dealloc(todo); break;
-            case vm_obj_kind::Closure:     to_composite(it)->dealloc(todo); break;
-            case vm_obj_kind::MPZ:         to_mpz_core(it)->dealloc(); break;
-            case vm_obj_kind::External:    to_external(it)->dealloc(); break;
+            case vm_obj_kind::Simple:        lean_unreachable();
+            case vm_obj_kind::Constructor:   to_composite(it)->dealloc(todo); break;
+            case vm_obj_kind::Closure:       to_composite(it)->dealloc(todo); break;
+            case vm_obj_kind::MPZ:           to_mpz_core(it)->dealloc(); break;
+            case vm_obj_kind::External:      to_external(it)->dealloc(); break;
+            case vm_obj_kind::NativeClosure: to_native_closure(it)->dealloc(todo); break;
             }
         }
     } catch (std::bad_alloc&) {
@@ -197,6 +297,14 @@ void display(std::ostream & out, vm_obj const & o, std::function<optional<name>(
             display(out, cfield(o, i), idx2name);
         }
         out << ")";
+    } else if (is_native_closure(o)) {
+        out << "([native_closure]";
+        vm_obj const * args = to_native_closure(o)->get_args();
+        for (unsigned i = 0; i < to_native_closure(o)->get_num_args(); i++) {
+            out << " ";
+            display(out, args[i], idx2name);
+        }
+        out << ")";
     } else {
         out << "[unknown]";
     }
@@ -1375,7 +1483,7 @@ vm_obj vm_state::invoke(vm_obj const & fn, vm_obj const & a1, vm_obj const & a2)
         }
     } else {
         lean_assert(nargs > d.get_arity());
-        return invoke(invoke(fn, a1), a2);
+        return ::lean::invoke(invoke(fn, a1), a2);
     }
 }
 
@@ -1415,9 +1523,9 @@ vm_obj vm_state::invoke(vm_obj const & fn, vm_obj const & a1, vm_obj const & a2,
             return invoke_closure(fn, 3);
         }
     } else if (nargs == d.get_arity() + 1) {
-        return invoke(invoke(fn, a1, a2), a3);
+        return ::lean::invoke(invoke(fn, a1, a2), a3);
     } else {
-        return invoke(invoke(fn, a1), a2, a3);
+        return ::lean::invoke(invoke(fn, a1), a2, a3);
     }
 }
 
@@ -1459,11 +1567,11 @@ vm_obj vm_state::invoke(vm_obj const & fn, vm_obj const & a1, vm_obj const & a2,
             return invoke_closure(fn, 4);
         }
     } else if (nargs == d.get_arity() + 1) {
-        return invoke(invoke(fn, a1, a2, a3), a4);
+        return ::lean::invoke(invoke(fn, a1, a2, a3), a4);
     } else if (nargs == d.get_arity() + 2) {
-        return invoke(invoke(fn, a1, a2), a3, a4);
+        return ::lean::invoke(invoke(fn, a1, a2), a3, a4);
     } else {
-        return invoke(invoke(fn, a1), a2, a3, a4);
+        return ::lean::invoke(invoke(fn, a1), a2, a3, a4);
     }
 }
 
@@ -1508,13 +1616,13 @@ vm_obj vm_state::invoke(vm_obj const & fn, vm_obj const & a1, vm_obj const & a2,
             return invoke_closure(fn, 5);
         }
     } else if (nargs == d.get_arity() + 1) {
-        return invoke(invoke(fn, a1, a2, a3, a4), a5);
+        return ::lean::invoke(invoke(fn, a1, a2, a3, a4), a5);
     } else if (nargs == d.get_arity() + 2) {
-        return invoke(invoke(fn, a1, a2, a3), a4, a5);
+        return ::lean::invoke(invoke(fn, a1, a2, a3), a4, a5);
     } else if (nargs == d.get_arity() + 3) {
-        return invoke(invoke(fn, a1, a2), a3, a4, a5);
+        return ::lean::invoke(invoke(fn, a1, a2), a3, a4, a5);
     } else {
-        return invoke(invoke(fn, a1), a2, a3, a4, a5);
+        return ::lean::invoke(invoke(fn, a1), a2, a3, a4, a5);
     }
 }
 
@@ -1561,15 +1669,15 @@ vm_obj vm_state::invoke(vm_obj const & fn, vm_obj const & a1, vm_obj const & a2,
             return invoke_closure(fn, 6);
         }
     } else if (nargs == d.get_arity() + 1) {
-        return invoke(invoke(fn, a1, a2, a3, a4, a5), a6);
+        return ::lean::invoke(invoke(fn, a1, a2, a3, a4, a5), a6);
     } else if (nargs == d.get_arity() + 2) {
-        return invoke(invoke(fn, a1, a2, a3, a4), a5, a6);
+        return ::lean::invoke(invoke(fn, a1, a2, a3, a4), a5, a6);
     } else if (nargs == d.get_arity() + 3) {
-        return invoke(invoke(fn, a1, a2, a3), a4, a5, a6);
+        return ::lean::invoke(invoke(fn, a1, a2, a3), a4, a5, a6);
     } else if (nargs == d.get_arity() + 4) {
-        return invoke(invoke(fn, a1, a2), a3, a4, a5, a6);
+        return ::lean::invoke(invoke(fn, a1, a2), a3, a4, a5, a6);
     } else {
-        return invoke(invoke(fn, a1), a2, a3, a4, a5, a6);
+        return ::lean::invoke(invoke(fn, a1), a2, a3, a4, a5, a6);
     }
 }
 
@@ -1618,17 +1726,17 @@ vm_obj vm_state::invoke(vm_obj const & fn, vm_obj const & a1, vm_obj const & a2,
             return invoke_closure(fn, 7);
         }
     } else if (nargs == d.get_arity() + 1) {
-        return invoke(invoke(fn, a1, a2, a3, a4, a5, a6), a7);
+        return ::lean::invoke(invoke(fn, a1, a2, a3, a4, a5, a6), a7);
     } else if (nargs == d.get_arity() + 2) {
-        return invoke(invoke(fn, a1, a2, a3, a4, a5), a6, a7);
+        return ::lean::invoke(invoke(fn, a1, a2, a3, a4, a5), a6, a7);
     } else if (nargs == d.get_arity() + 3) {
-        return invoke(invoke(fn, a1, a2, a3, a4), a5, a6, a7);
+        return ::lean::invoke(invoke(fn, a1, a2, a3, a4), a5, a6, a7);
     } else if (nargs == d.get_arity() + 4) {
-        return invoke(invoke(fn, a1, a2, a3), a4, a5, a6, a7);
+        return ::lean::invoke(invoke(fn, a1, a2, a3), a4, a5, a6, a7);
     } else if (nargs == d.get_arity() + 5) {
-        return invoke(invoke(fn, a1, a2), a3, a4, a5, a6, a7);
+        return ::lean::invoke(invoke(fn, a1, a2), a3, a4, a5, a6, a7);
     } else {
-        return invoke(invoke(fn, a1), a2, a3, a4, a5, a6, a7);
+        return ::lean::invoke(invoke(fn, a1), a2, a3, a4, a5, a6, a7);
     }
 }
 
@@ -1679,19 +1787,19 @@ vm_obj vm_state::invoke(vm_obj const & fn, vm_obj const & a1, vm_obj const & a2,
             return invoke_closure(fn, 8);
         }
     } else if (nargs == d.get_arity() + 1) {
-        return invoke(invoke(fn, a1, a2, a3, a4, a5, a6, a7), a8);
+        return ::lean::invoke(invoke(fn, a1, a2, a3, a4, a5, a6, a7), a8);
     } else if (nargs == d.get_arity() + 2) {
-        return invoke(invoke(fn, a1, a2, a3, a4, a5, a6), a7, a8);
+        return ::lean::invoke(invoke(fn, a1, a2, a3, a4, a5, a6), a7, a8);
     } else if (nargs == d.get_arity() + 3) {
-        return invoke(invoke(fn, a1, a2, a3, a4, a5), a6, a7, a8);
+        return ::lean::invoke(invoke(fn, a1, a2, a3, a4, a5), a6, a7, a8);
     } else if (nargs == d.get_arity() + 4) {
-        return invoke(invoke(fn, a1, a2, a3, a4), a5, a6, a7, a8);
+        return ::lean::invoke(invoke(fn, a1, a2, a3, a4), a5, a6, a7, a8);
     } else if (nargs == d.get_arity() + 5) {
-        return invoke(invoke(fn, a1, a2, a3), a4, a5, a6, a7, a8);
+        return ::lean::invoke(invoke(fn, a1, a2, a3), a4, a5, a6, a7, a8);
     } else if (nargs == d.get_arity() + 6) {
-        return invoke(invoke(fn, a1, a2), a3, a4, a5, a6, a7, a8);
+        return ::lean::invoke(invoke(fn, a1, a2), a3, a4, a5, a6, a7, a8);
     } else {
-        return invoke(invoke(fn, a1), a2, a3, a4, a5, a6, a7, a8);
+        return ::lean::invoke(invoke(fn, a1), a2, a3, a4, a5, a6, a7, a8);
     }
 }
 
@@ -1734,7 +1842,7 @@ vm_obj vm_state::invoke(vm_obj const & fn, unsigned nargs, vm_obj const * args)
             return invoke_closure(fn, nargs);
         }
     } else {
-        lean_assert(nargs + csize(fn) > d.get_arity());
+        lean_assert(new_nargs > d.get_arity());
         buffer<vm_obj> new_args;
         buffer<vm_obj> rest_args;
         /* copy arity - csize(fn) arguments to new_args, and the rest to rest_args */
@@ -1744,57 +1852,107 @@ vm_obj vm_state::invoke(vm_obj const & fn, unsigned nargs, vm_obj const * args)
         lean_assert(n < nargs);
         new_args.append(n, args);
         rest_args.append(nargs - n, args + n);
-        return invoke(invoke(fn, new_args.size(), new_args.data()), rest_args.size(), rest_args.data());
+        return ::lean::invoke(invoke(fn, new_args.size(), new_args.data()), rest_args.size(), rest_args.data());
     }
 }
 
+vm_obj native_invoke(vm_obj const & fn, vm_obj const & a1);
+vm_obj native_invoke(vm_obj const & fn, vm_obj const & a1, vm_obj const & a2);
+vm_obj native_invoke(vm_obj const & fn, vm_obj const & a1, vm_obj const & a2, vm_obj const & a3);
+vm_obj native_invoke(vm_obj const & fn, vm_obj const & a1, vm_obj const & a2, vm_obj const & a3, vm_obj const & a4);
+vm_obj native_invoke(vm_obj const & fn, vm_obj const & a1, vm_obj const & a2, vm_obj const & a3, vm_obj const & a4,
+                     vm_obj const & a5);
+vm_obj native_invoke(vm_obj const & fn, vm_obj const & a1, vm_obj const & a2, vm_obj const & a3, vm_obj const & a4,
+                     vm_obj const & a5, vm_obj const & a6);
+vm_obj native_invoke(vm_obj const & fn, vm_obj const & a1, vm_obj const & a2, vm_obj const & a3, vm_obj const & a4,
+                     vm_obj const & a5, vm_obj const & a6, vm_obj const & a7);
+vm_obj native_invoke(vm_obj const & fn, vm_obj const & a1, vm_obj const & a2, vm_obj const & a3, vm_obj const & a4,
+                     vm_obj const & a5, vm_obj const & a6, vm_obj const & a7, vm_obj const & a8);
+vm_obj native_invoke(vm_obj const & fn, unsigned nargs, vm_obj const * args);
+
 vm_obj invoke(vm_obj const & fn, vm_obj const & a1) {
-    lean_assert(g_vm_state);
-    return g_vm_state->invoke(fn, a1);
+    if (is_native_closure(fn)) {
+        return native_invoke(fn, a1);
+    } else {
+        lean_assert(g_vm_state);
+        return g_vm_state->invoke(fn, a1);
+    }
 }
 
 vm_obj invoke(vm_obj const & fn, vm_obj const & a1, vm_obj const & a2) {
-    lean_assert(g_vm_state);
-    return g_vm_state->invoke(fn, a1, a2);
+    if (is_native_closure(fn)) {
+        return native_invoke(fn, a1, a2);
+    } else {
+        lean_assert(g_vm_state);
+        return g_vm_state->invoke(fn, a1, a2);
+    }
 }
 
 vm_obj invoke(vm_obj const & fn, vm_obj const & a1, vm_obj const & a2, vm_obj const & a3) {
-    lean_assert(g_vm_state);
-    return g_vm_state->invoke(fn, a1, a2, a3);
+    if (is_native_closure(fn)) {
+        return native_invoke(fn, a1, a2);
+    } else {
+        lean_assert(g_vm_state);
+        return g_vm_state->invoke(fn, a1, a2, a3);
+    }
 }
 
 vm_obj invoke(vm_obj const & fn, vm_obj const & a1, vm_obj const & a2, vm_obj const & a3, vm_obj const & a4) {
-    lean_assert(g_vm_state);
-    return g_vm_state->invoke(fn, a1, a2, a3, a4);
+    if (is_native_closure(fn)) {
+        return native_invoke(fn, a1, a2, a3, a4);
+    } else {
+        lean_assert(g_vm_state);
+        return g_vm_state->invoke(fn, a1, a2, a3, a4);
+    }
 }
 
 vm_obj invoke(vm_obj const & fn, vm_obj const & a1, vm_obj const & a2, vm_obj const & a3, vm_obj const & a4,
               vm_obj const & a5) {
-    lean_assert(g_vm_state);
-    return g_vm_state->invoke(fn, a1, a2, a3, a4, a5);
+    if (is_native_closure(fn)) {
+        return native_invoke(fn, a1, a2, a3, a4, a5);
+    } else {
+        lean_assert(g_vm_state);
+        return g_vm_state->invoke(fn, a1, a2, a3, a4, a5);
+    }
 }
 
 vm_obj invoke(vm_obj const & fn, vm_obj const & a1, vm_obj const & a2, vm_obj const & a3, vm_obj const & a4,
               vm_obj const & a5, vm_obj const & a6) {
-    lean_assert(g_vm_state);
-    return g_vm_state->invoke(fn, a1, a2, a3, a4, a5, a6);
+    if (is_native_closure(fn)) {
+        return native_invoke(fn, a1, a2, a3, a4, a5, a6);
+    } else {
+        lean_assert(g_vm_state);
+        return g_vm_state->invoke(fn, a1, a2, a3, a4, a5, a6);
+    }
 }
 
 vm_obj invoke(vm_obj const & fn, vm_obj const & a1, vm_obj const & a2, vm_obj const & a3, vm_obj const & a4,
               vm_obj const & a5, vm_obj const & a6, vm_obj const & a7) {
-    lean_assert(g_vm_state);
-    return g_vm_state->invoke(fn, a1, a2, a3, a4, a5, a6, a7);
+    if (is_native_closure(fn)) {
+        return native_invoke(fn, a1, a2, a3, a4, a5, a6, a7);
+    } else {
+        lean_assert(g_vm_state);
+        return g_vm_state->invoke(fn, a1, a2, a3, a4, a5, a6, a7);
+    }
 }
 
 vm_obj invoke(vm_obj const & fn, vm_obj const & a1, vm_obj const & a2, vm_obj const & a3, vm_obj const & a4,
               vm_obj const & a5, vm_obj const & a6, vm_obj const & a7, vm_obj const & a8) {
-    lean_assert(g_vm_state);
-    return g_vm_state->invoke(fn, a1, a2, a3, a4, a5, a6, a7, a8);
+    if (is_native_closure(fn)) {
+        return native_invoke(fn, a1, a2, a3, a4, a5, a6, a7, a8);
+    } else {
+        lean_assert(g_vm_state);
+        return g_vm_state->invoke(fn, a1, a2, a3, a4, a5, a6, a7, a8);
+    }
 }
 
 vm_obj invoke(vm_obj const & fn, unsigned nargs, vm_obj const * args) {
-    lean_assert(g_vm_state);
-    return g_vm_state->invoke(fn, nargs, args);
+    if (is_native_closure(fn)) {
+        return native_invoke(fn, nargs, args);
+    } else {
+        lean_assert(g_vm_state);
+        return g_vm_state->invoke(fn, nargs, args);
+    }
 }
 
 vm_obj invoke(unsigned fn_idx, unsigned nargs, vm_obj const * args) {
@@ -1807,6 +1965,419 @@ vm_obj invoke(unsigned fn_idx, vm_obj const & arg) {
     return invoke(fn_idx, 1, &arg);
 }
 
+static vm_obj update_native_closure(vm_obj const & fn, buffer<vm_obj> const & new_args) {
+    vm_native_closure const * c = to_native_closure(fn);
+    lean_assert(new_args.size() < c->get_arity());
+    return mk_native_closure(c->get_fn(), c->get_arity(), new_args.size(), new_args.data());
+}
+
+inline vm_cfunction_1 to_nfn1(vm_obj const & fn) { return reinterpret_cast<vm_cfunction_1>(to_native_closure(fn)->get_fn()); }
+inline vm_cfunction_2 to_nfn2(vm_obj const & fn) { return reinterpret_cast<vm_cfunction_2>(to_native_closure(fn)->get_fn()); }
+inline vm_cfunction_3 to_nfn3(vm_obj const & fn) { return reinterpret_cast<vm_cfunction_3>(to_native_closure(fn)->get_fn()); }
+inline vm_cfunction_4 to_nfn4(vm_obj const & fn) { return reinterpret_cast<vm_cfunction_4>(to_native_closure(fn)->get_fn()); }
+inline vm_cfunction_5 to_nfn5(vm_obj const & fn) { return reinterpret_cast<vm_cfunction_5>(to_native_closure(fn)->get_fn()); }
+inline vm_cfunction_6 to_nfn6(vm_obj const & fn) { return reinterpret_cast<vm_cfunction_6>(to_native_closure(fn)->get_fn()); }
+inline vm_cfunction_7 to_nfn7(vm_obj const & fn) { return reinterpret_cast<vm_cfunction_7>(to_native_closure(fn)->get_fn()); }
+inline vm_cfunction_8 to_nfn8(vm_obj const & fn) { return reinterpret_cast<vm_cfunction_8>(to_native_closure(fn)->get_fn()); }
+inline vm_cfunction_N to_nfnN(vm_obj const & fn) { return reinterpret_cast<vm_cfunction_N>(to_native_closure(fn)->get_fn()); }
+
+static void append_native_args(vm_obj const & fn, buffer<vm_obj> & args) {
+    lean_assert(is_native_closure(fn));
+    vm_obj const * begin = to_native_closure(fn)->get_args();
+    vm_obj const * end   = begin + to_native_closure(fn)->get_num_args();
+    vm_obj const * it    = end;
+    while (it != begin) {
+        --it;
+        args.push_back(*it);
+    }
+}
+
+vm_obj native_invoke(vm_obj const & fn, vm_obj const & a1) {
+    vm_native_closure const * c = to_native_closure(fn);
+    unsigned nargs      = c->get_num_args();
+    vm_obj const * args = c->get_args();
+    unsigned arity      = c->get_arity();
+    unsigned new_nargs  = nargs + 1;
+    if (new_nargs < arity) {
+        buffer<vm_obj> new_args;
+        new_args.push_back(a1);
+        new_args.append(nargs, args);
+        return update_native_closure(fn, new_args);
+    } else {
+        switch (arity) {
+        case 0: lean_unreachable();
+        case 1: return to_nfn1(fn)(a1);
+        case 2: return to_nfn2(fn)(args[0], a1);
+        case 3: return to_nfn3(fn)(args[1], args[0], a1);
+        case 4: return to_nfn4(fn)(args[2], args[1], args[0], a1);
+        case 5: return to_nfn5(fn)(args[3], args[2], args[1], args[0], a1);
+        case 6: return to_nfn6(fn)(args[4], args[3], args[2], args[1], args[0], a1);
+        case 7: return to_nfn7(fn)(args[5], args[4], args[3], args[2], args[1], args[0], a1);
+        case 8: return to_nfn8(fn)(args[6], args[5], args[4], args[3], args[2], args[1], args[0], a1);
+        default:
+            buffer<vm_obj> new_args;
+            append_native_args(fn, new_args);
+            new_args.push_back(a1);
+            return to_nfnN(fn)(new_args.size(), new_args.data());
+        }
+    }
+}
+
+vm_obj native_invoke(vm_obj const & fn, vm_obj const & a1, vm_obj const & a2) {
+    vm_native_closure const * c = to_native_closure(fn);
+    unsigned nargs      = c->get_num_args();
+    vm_obj const * args = c->get_args();
+    unsigned arity      = c->get_arity();
+    unsigned new_nargs  = nargs + 2;
+    if (new_nargs < arity) {
+        buffer<vm_obj> new_args;
+        new_args.push_back(a2);
+        new_args.push_back(a1);
+        new_args.append(nargs, args);
+        return update_native_closure(fn, new_args);
+    } else if (new_nargs == arity) {
+        switch (arity) {
+        case 0: case 1: lean_unreachable();
+        case 2: return to_nfn2(fn)(a1, a2);
+        case 3: return to_nfn3(fn)(args[0], a1, a2);
+        case 4: return to_nfn4(fn)(args[1], args[0], a1, a2);
+        case 5: return to_nfn5(fn)(args[2], args[1], args[0], a1, a2);
+        case 6: return to_nfn6(fn)(args[3], args[2], args[1], args[0], a1, a2);
+        case 7: return to_nfn7(fn)(args[4], args[3], args[2], args[1], args[0], a1, a2);
+        case 8: return to_nfn8(fn)(args[5], args[4], args[3], args[2], args[1], args[0], a1, a2);
+        default:
+            buffer<vm_obj> new_args;
+            append_native_args(fn, new_args);
+            new_args.push_back(a1);
+            new_args.push_back(a2);
+            return to_nfnN(fn)(new_args.size(), new_args.data());
+        }
+    } else {
+        lean_assert(new_nargs > arity);
+        return invoke(native_invoke(fn, a1), a2);
+    }
+}
+
+vm_obj native_invoke(vm_obj const & fn, vm_obj const & a1, vm_obj const & a2, vm_obj const & a3) {
+    vm_native_closure const * c = to_native_closure(fn);
+    unsigned nargs      = c->get_num_args();
+    vm_obj const * args = c->get_args();
+    unsigned arity      = c->get_arity();
+    unsigned new_nargs  = nargs + 3;
+    if (new_nargs < arity) {
+        buffer<vm_obj> new_args;
+        new_args.push_back(a3);
+        new_args.push_back(a2);
+        new_args.push_back(a1);
+        new_args.append(nargs, args);
+        return update_native_closure(fn, new_args);
+    } else if (new_nargs == arity) {
+        switch (arity) {
+        case 0: case 1: case 2: lean_unreachable();
+        case 3: return to_nfn3(fn)(a1, a2, a3);
+        case 4: return to_nfn4(fn)(args[0], a1, a2, a3);
+        case 5: return to_nfn5(fn)(args[1], args[0], a1, a2, a3);
+        case 6: return to_nfn6(fn)(args[2], args[1], args[0], a1, a2, a3);
+        case 7: return to_nfn7(fn)(args[3], args[2], args[1], args[0], a1, a2, a3);
+        case 8: return to_nfn8(fn)(args[4], args[3], args[2], args[1], args[0], a1, a2, a3);
+        default:
+            buffer<vm_obj> new_args;
+            append_native_args(fn, new_args);
+            new_args.push_back(a1);
+            new_args.push_back(a2);
+            new_args.push_back(a3);
+            return to_nfnN(fn)(new_args.size(), new_args.data());
+        }
+    } else if (new_nargs == arity + 1) {
+        return invoke(native_invoke(fn, a1, a2), a3);
+    } else {
+        return invoke(native_invoke(fn, a1), a2, a3);
+    }
+}
+
+vm_obj native_invoke(vm_obj const & fn, vm_obj const & a1, vm_obj const & a2, vm_obj const & a3, vm_obj const & a4) {
+    vm_native_closure const * c = to_native_closure(fn);
+    unsigned nargs      = c->get_num_args();
+    vm_obj const * args = c->get_args();
+    unsigned arity      = c->get_arity();
+    unsigned new_nargs  = nargs + 4;
+    if (new_nargs < arity) {
+        buffer<vm_obj> new_args;
+        new_args.push_back(a4);
+        new_args.push_back(a3);
+        new_args.push_back(a2);
+        new_args.push_back(a1);
+        new_args.append(nargs, args);
+        return update_native_closure(fn, new_args);
+    } else if (new_nargs == arity) {
+        switch (arity) {
+        case 0: case 1: case 2: case 3: lean_unreachable();
+        case 4: return to_nfn4(fn)(a1, a2, a3, a4);
+        case 5: return to_nfn5(fn)(args[0], a1, a2, a3, a4);
+        case 6: return to_nfn6(fn)(args[1], args[0], a1, a2, a3, a4);
+        case 7: return to_nfn7(fn)(args[2], args[1], args[0], a1, a2, a3, a4);
+        case 8: return to_nfn8(fn)(args[3], args[2], args[1], args[0], a1, a2, a3, a4);
+        default:
+            buffer<vm_obj> new_args;
+            append_native_args(fn, new_args);
+            new_args.push_back(a1);
+            new_args.push_back(a2);
+            new_args.push_back(a3);
+            new_args.push_back(a4);
+            return to_nfnN(fn)(new_args.size(), new_args.data());
+        }
+    } else if (new_nargs == arity + 1) {
+        return invoke(native_invoke(fn, a1, a2, a3), a4);
+    } else if (new_nargs == arity + 2) {
+        return invoke(native_invoke(fn, a1, a2), a3, a4);
+    } else {
+        return invoke(native_invoke(fn, a1), a2, a3, a4);
+    }
+}
+
+vm_obj native_invoke(vm_obj const & fn, vm_obj const & a1, vm_obj const & a2, vm_obj const & a3, vm_obj const & a4,
+                     vm_obj const & a5) {
+    vm_native_closure const * c = to_native_closure(fn);
+    unsigned nargs      = c->get_num_args();
+    vm_obj const * args = c->get_args();
+    unsigned arity      = c->get_arity();
+    unsigned new_nargs  = nargs + 5;
+    if (new_nargs < arity) {
+        buffer<vm_obj> new_args;
+        new_args.push_back(a5);
+        new_args.push_back(a4);
+        new_args.push_back(a3);
+        new_args.push_back(a2);
+        new_args.push_back(a1);
+        new_args.append(nargs, args);
+        return update_native_closure(fn, new_args);
+    } else if (new_nargs == arity) {
+        switch (arity) {
+        case 0: case 1: case 2: case 3: case 4: lean_unreachable();
+        case 5: return to_nfn5(fn)(a1, a2, a3, a4, a5);
+        case 6: return to_nfn6(fn)(args[0], a1, a2, a3, a4, a5);
+        case 7: return to_nfn7(fn)(args[1], args[0], a1, a2, a3, a4, a5);
+        case 8: return to_nfn8(fn)(args[2], args[1], args[0], a1, a2, a3, a4, a5);
+        default:
+            buffer<vm_obj> new_args;
+            append_native_args(fn, new_args);
+            new_args.push_back(a1);
+            new_args.push_back(a2);
+            new_args.push_back(a3);
+            new_args.push_back(a4);
+            new_args.push_back(a5);
+            return to_nfnN(fn)(new_args.size(), new_args.data());
+        }
+    } else if (new_nargs == arity + 1) {
+        return invoke(native_invoke(fn, a1, a2, a3, a4), a5);
+    } else if (new_nargs == arity + 2) {
+        return invoke(native_invoke(fn, a1, a2, a3), a4, a5);
+    } else if (new_nargs == arity + 3) {
+        return invoke(native_invoke(fn, a1, a2), a3, a4, a5);
+    } else {
+        return invoke(native_invoke(fn, a1), a2, a3, a4, a5);
+    }
+}
+
+vm_obj native_invoke(vm_obj const & fn, vm_obj const & a1, vm_obj const & a2, vm_obj const & a3, vm_obj const & a4,
+                     vm_obj const & a5, vm_obj const & a6) {
+    vm_native_closure const * c = to_native_closure(fn);
+    unsigned nargs      = c->get_num_args();
+    vm_obj const * args = c->get_args();
+    unsigned arity      = c->get_arity();
+    unsigned new_nargs  = nargs + 6;
+    if (new_nargs < arity) {
+        buffer<vm_obj> new_args;
+        new_args.push_back(a6);
+        new_args.push_back(a5);
+        new_args.push_back(a4);
+        new_args.push_back(a3);
+        new_args.push_back(a2);
+        new_args.push_back(a1);
+        new_args.append(nargs, args);
+        return update_native_closure(fn, new_args);
+    } else if (new_nargs == arity) {
+        switch (arity) {
+        case 0: case 1: case 2: case 3: case 4: case 5: lean_unreachable();
+        case 6: return to_nfn6(fn)(a1, a2, a3, a4, a5, a6);
+        case 7: return to_nfn7(fn)(args[0], a1, a2, a3, a4, a5, a6);
+        case 8: return to_nfn8(fn)(args[1], args[0], a1, a2, a3, a4, a5, a6);
+        default:
+            buffer<vm_obj> new_args;
+            append_native_args(fn, new_args);
+            new_args.push_back(a1);
+            new_args.push_back(a2);
+            new_args.push_back(a3);
+            new_args.push_back(a4);
+            new_args.push_back(a5);
+            new_args.push_back(a6);
+            return to_nfnN(fn)(new_args.size(), new_args.data());
+        }
+    } else if (new_nargs == arity + 1) {
+        return invoke(native_invoke(fn, a1, a2, a3, a4, a5), a6);
+    } else if (new_nargs == arity + 2) {
+        return invoke(native_invoke(fn, a1, a2, a3, a4), a5, a6);
+    } else if (new_nargs == arity + 3) {
+        return invoke(native_invoke(fn, a1, a2, a3), a4, a5, a6);
+    } else if (new_nargs == arity + 4) {
+        return invoke(native_invoke(fn, a1, a2), a3, a4, a5, a6);
+    } else {
+        return invoke(native_invoke(fn, a1), a2, a3, a4, a5, a6);
+    }
+}
+
+vm_obj native_invoke(vm_obj const & fn, vm_obj const & a1, vm_obj const & a2, vm_obj const & a3, vm_obj const & a4,
+                     vm_obj const & a5, vm_obj const & a6, vm_obj const & a7) {
+    vm_native_closure const * c = to_native_closure(fn);
+    unsigned nargs      = c->get_num_args();
+    vm_obj const * args = c->get_args();
+    unsigned arity      = c->get_arity();
+    unsigned new_nargs  = nargs + 7;
+    if (new_nargs < arity) {
+        buffer<vm_obj> new_args;
+        new_args.push_back(a7);
+        new_args.push_back(a6);
+        new_args.push_back(a5);
+        new_args.push_back(a4);
+        new_args.push_back(a3);
+        new_args.push_back(a2);
+        new_args.push_back(a1);
+        new_args.append(nargs, args);
+        return update_native_closure(fn, new_args);
+    } else if (new_nargs == arity) {
+        switch (arity) {
+        case 0: case 1: case 2: case 3: case 4: case 5: case 6: lean_unreachable();
+        case 7: return to_nfn7(fn)(a1, a2, a3, a4, a5, a6, a7);
+        case 8: return to_nfn8(fn)(args[0], a1, a2, a3, a4, a5, a6, a7);
+        default:
+            buffer<vm_obj> new_args;
+            append_native_args(fn, new_args);
+            new_args.push_back(a1);
+            new_args.push_back(a2);
+            new_args.push_back(a3);
+            new_args.push_back(a4);
+            new_args.push_back(a5);
+            new_args.push_back(a6);
+            new_args.push_back(a7);
+            return to_nfnN(fn)(new_args.size(), new_args.data());
+        }
+    } else if (new_nargs == arity + 1) {
+        return invoke(native_invoke(fn, a1, a2, a3, a4, a5, a6), a7);
+    } else if (new_nargs == arity + 2) {
+        return invoke(native_invoke(fn, a1, a2, a3, a4, a5), a6, a7);
+    } else if (new_nargs == arity + 3) {
+        return invoke(native_invoke(fn, a1, a2, a3, a4), a5, a6, a7);
+    } else if (new_nargs == arity + 4) {
+        return invoke(native_invoke(fn, a1, a2, a3), a4, a5, a6, a7);
+    } else if (new_nargs == arity + 5) {
+        return invoke(native_invoke(fn, a1, a2), a3, a4, a5, a6, a7);
+    } else {
+        return invoke(native_invoke(fn, a1), a2, a3, a4, a5, a6, a7);
+    }
+}
+
+vm_obj native_invoke(vm_obj const & fn, vm_obj const & a1, vm_obj const & a2, vm_obj const & a3, vm_obj const & a4,
+                     vm_obj const & a5, vm_obj const & a6, vm_obj const & a7, vm_obj const & a8) {
+    vm_native_closure const * c = to_native_closure(fn);
+    unsigned nargs      = c->get_num_args();
+    vm_obj const * args = c->get_args();
+    unsigned arity      = c->get_arity();
+    unsigned new_nargs  = nargs + 8;
+    if (new_nargs < arity) {
+        buffer<vm_obj> new_args;
+        new_args.push_back(a8);
+        new_args.push_back(a7);
+        new_args.push_back(a6);
+        new_args.push_back(a5);
+        new_args.push_back(a4);
+        new_args.push_back(a3);
+        new_args.push_back(a2);
+        new_args.push_back(a1);
+        new_args.append(nargs, args);
+        return update_native_closure(fn, new_args);
+    } else if (new_nargs == arity) {
+        switch (arity) {
+        case 0: case 1: case 2: case 3: case 4: case 5: case 6: case 7: lean_unreachable();
+        case 8: return to_nfn8(fn)(a1, a2, a3, a4, a5, a6, a7, a8);
+        default:
+            buffer<vm_obj> new_args;
+            append_native_args(fn, new_args);
+            new_args.push_back(a1);
+            new_args.push_back(a2);
+            new_args.push_back(a3);
+            new_args.push_back(a4);
+            new_args.push_back(a5);
+            new_args.push_back(a6);
+            new_args.push_back(a7);
+            new_args.push_back(a8);
+            return to_nfnN(fn)(new_args.size(), new_args.data());
+        }
+    } else if (new_nargs == arity + 1) {
+        return invoke(native_invoke(fn, a1, a2, a3, a4, a5, a6, a7), a8);
+    } else if (new_nargs == arity + 2) {
+        return invoke(native_invoke(fn, a1, a2, a3, a4, a5, a6), a7, a8);
+    } else if (new_nargs == arity + 3) {
+        return invoke(native_invoke(fn, a1, a2, a3, a4, a5), a6, a7, a8);
+    } else if (new_nargs == arity + 4) {
+        return invoke(native_invoke(fn, a1, a2, a3, a4), a5, a6, a7, a8);
+    } else if (new_nargs == arity + 5) {
+        return invoke(native_invoke(fn, a1, a2, a3), a4, a5, a6, a7, a8);
+    } else if (new_nargs == arity + 6) {
+        return invoke(native_invoke(fn, a1, a2), a3, a4, a5, a6, a7, a8);
+    } else {
+        return invoke(native_invoke(fn, a1), a2, a3, a4, a5, a6, a7, a8);
+    }
+}
+
+vm_obj native_invoke(vm_obj const & fn, unsigned nargs, vm_obj const * args) {
+    if (nargs <= 8) {
+        switch (nargs) {
+        case 1: return native_invoke(fn, args[0]);
+        case 2: return native_invoke(fn, args[0], args[1]);
+        case 3: return native_invoke(fn, args[0], args[1], args[2]);
+        case 4: return native_invoke(fn, args[0], args[1], args[2], args[3]);
+        case 5: return native_invoke(fn, args[0], args[1], args[2], args[3], args[4]);
+        case 6: return native_invoke(fn, args[0], args[1], args[2], args[3], args[4], args[5]);
+        case 7: return native_invoke(fn, args[0], args[1], args[2], args[3], args[4], args[5], args[6]);
+        case 8: return native_invoke(fn, args[0], args[1], args[2], args[3], args[4], args[5], args[6], args[7]);
+        default: lean_unreachable();
+        }
+    }
+    vm_native_closure const * c = to_native_closure(fn);
+    unsigned c_nargs      = c->get_num_args();
+    vm_obj const * c_args = c->get_args();
+    unsigned arity        = c->get_arity();
+    unsigned new_c_nargs  = c_nargs + nargs;
+    if (new_c_nargs < arity) {
+        buffer<vm_obj> new_args;
+        unsigned i = nargs;
+        while (i > 0) { --i; new_args.push_back(args[i]); }
+        new_args.append(c_nargs, c_args);
+        return update_native_closure(fn, new_args);
+    } else if (new_c_nargs == arity) {
+        if (c_nargs == 0) {
+            return to_nfnN(fn)(nargs, args);
+        } else {
+            buffer<vm_obj> new_args;
+            append_native_args(fn, new_args);
+            new_args.append(nargs, args);
+            return to_nfnN(fn)(nargs, args);
+        }
+    } else {
+        lean_assert(new_c_nargs > arity);
+        buffer<vm_obj> new_args;
+        buffer<vm_obj> rest_args;
+        /* copy arity - csize(fn) arguments to new_args, and the rest to rest_args */
+        lean_assert(c_nargs < arity);
+        unsigned n = arity - c_nargs;
+        lean_assert(n > 1);
+        lean_assert(n < nargs);
+        new_args.append(n, args);
+        rest_args.append(nargs - n, args + n);
+        return invoke(native_invoke(fn, new_args.size(), new_args.data()), rest_args.size(), rest_args.data());
+    }
+}
+
 vm_state & get_vm_state() {
     lean_assert(g_vm_state);
     return *g_vm_state;
@@ -2259,34 +2830,41 @@ void vm_state::run() {
             unsigned sz       = m_stack.size();
             vm_obj closure    = m_stack.back();
             stack_pop_back();
-            unsigned fn_idx   = cfn_idx(closure);
-            vm_decl d         = get_decl(fn_idx);
-            unsigned csz      = csize(closure);
-            unsigned arity    = d.get_arity();
-            lean_assert(csz < arity);
-            unsigned nargs    = csz + 1;
-            lean_assert(nargs <= arity);
-            /* Keep consuming 'apply' instructions while nargs < arity */
-            while (nargs < arity && m_code[m_pc+1].op() == opcode::Apply) {
-                nargs++;
-                m_pc++;
-            }
-            /* Copy closure data to the top of the stack */
-            std::copy(cfields(closure), cfields(closure) + csz, std::back_inserter(m_stack));
-            if (nargs < arity) {
-                /* Case 1) We don't have sufficient arguments. So, we create a new closure */
-                sz = m_stack.size();
-                vm_obj new_value = mk_vm_closure(fn_idx, nargs, m_stack.data() + sz - nargs);
-                m_stack.resize(sz - nargs + 1);
-                swap(m_stack.back(), new_value);
-                if (m_debugging) shrink_stack_info();
-                m_pc++;
-                goto main_loop;
+            if (is_native_closure(closure)) {
+                // NOT IMPLEMENTED YET.
+                // This branch can only be reached if we mix bytecode and generated C++ code.
+                // TODO(Leo): we need to be able to dynamic link generated C++ code to be able to test this branch.
+                lean_unreachable();
             } else {
-                lean_assert(nargs == arity);
-                /* Case 2 */
-                invoke(d);
-                goto main_loop;
+                unsigned fn_idx   = cfn_idx(closure);
+                vm_decl d         = get_decl(fn_idx);
+                unsigned csz      = csize(closure);
+                unsigned arity    = d.get_arity();
+                lean_assert(csz < arity);
+                unsigned nargs    = csz + 1;
+                lean_assert(nargs <= arity);
+                /* Keep consuming 'apply' instructions while nargs < arity */
+                while (nargs < arity && m_code[m_pc+1].op() == opcode::Apply) {
+                    nargs++;
+                    m_pc++;
+                }
+                /* Copy closure data to the top of the stack */
+                std::copy(cfields(closure), cfields(closure) + csz, std::back_inserter(m_stack));
+                if (nargs < arity) {
+                    /* Case 1) We don't have sufficient arguments. So, we create a new closure */
+                    sz = m_stack.size();
+                    vm_obj new_value = mk_vm_closure(fn_idx, nargs, m_stack.data() + sz - nargs);
+                    m_stack.resize(sz - nargs + 1);
+                    swap(m_stack.back(), new_value);
+                    if (m_debugging) shrink_stack_info();
+                    m_pc++;
+                    goto main_loop;
+                } else {
+                    lean_assert(nargs == arity);
+                    /* Case 2 */
+                    invoke(d);
+                    goto main_loop;
+                }
             }
         }
         case opcode::InvokeGlobal: {
diff --git a/src/library/vm/vm.h b/src/library/vm/vm.h
index d6b879ce88..0596ce0a20 100644
--- a/src/library/vm/vm.h
+++ b/src/library/vm/vm.h
@@ -20,7 +20,7 @@ Author: Leonardo de Moura
 
 namespace lean {
 class vm_obj;
-enum class vm_obj_kind { Simple, Constructor, Closure, MPZ, External };
+enum class vm_obj_kind { Simple, Constructor, Closure, NativeClosure, MPZ, External };
 
 /** \brief Base class for VM objects.
 
@@ -135,6 +135,45 @@ public:
     ~vm_external() {}
 };
 
+/** Builtin functions that take arguments from the system stack.
+
+    \remark The C++ code generator produces this kind of function. */
+typedef vm_obj (*vm_cfunction)(vm_obj const &);
+typedef vm_obj (*vm_cfunction_0)();
+typedef vm_obj (*vm_cfunction_1)(vm_obj const &);
+typedef vm_obj (*vm_cfunction_2)(vm_obj const &, vm_obj const &);
+typedef vm_obj (*vm_cfunction_3)(vm_obj const &, vm_obj const &, vm_obj const &);
+typedef vm_obj (*vm_cfunction_4)(vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &);
+typedef vm_obj (*vm_cfunction_5)(vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &,
+                                 vm_obj const &);
+typedef vm_obj (*vm_cfunction_6)(vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &,
+                                 vm_obj const &, vm_obj const &);
+typedef vm_obj (*vm_cfunction_7)(vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &,
+                                 vm_obj const &, vm_obj const &, vm_obj const &);
+typedef vm_obj (*vm_cfunction_8)(vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &,
+                                 vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &);
+typedef vm_obj (*vm_cfunction_N)(unsigned n, vm_obj const *);
+
+/* Closure for C++ generated code, they do not require a vm_state object to be used. */
+class vm_native_closure : public vm_obj_cell {
+    vm_cfunction m_fn;
+    unsigned     m_arity;
+    unsigned     m_num_args;
+    vm_obj * get_args_ptr() {
+        return reinterpret_cast<vm_obj *>(reinterpret_cast<char *>(this)+sizeof(vm_native_closure));
+    }
+    friend vm_obj_cell;
+    void dealloc(buffer<vm_obj_cell*> & todelete);
+public:
+    vm_native_closure(vm_cfunction fn, unsigned arity, unsigned num_args, vm_obj const * args);
+    vm_cfunction get_fn() const { return m_fn; }
+    unsigned get_arity() const { return m_arity; }
+    unsigned get_num_args() const { return m_num_args; }
+    vm_obj const * get_args() const {
+        return reinterpret_cast<vm_obj const *>(reinterpret_cast<char const *>(this)+sizeof(vm_native_closure));
+    }
+};
+
 small_object_allocator & get_vm_allocator();
 
 // =======================================
@@ -146,9 +185,30 @@ vm_obj mk_vm_constructor(unsigned cidx, vm_obj const &);
 vm_obj mk_vm_constructor(unsigned cidx, vm_obj const &, vm_obj const &);
 vm_obj mk_vm_constructor(unsigned cidx, vm_obj const &, vm_obj const &, vm_obj const &);
 vm_obj mk_vm_constructor(unsigned cidx, vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &);
-vm_obj mk_vm_closure(unsigned fnidx, unsigned sz, vm_obj const * args);
+/* TODO(Leo, Jared): delete native closures that take environment as argument */
 vm_obj mk_native_closure(environment const & env, name const & n, unsigned sz, vm_obj const * args);
 vm_obj mk_native_closure(environment const & env, name const & n, std::initializer_list<vm_obj const> args);
+/* Native closures */
+vm_obj mk_native_closure(vm_cfunction_1 fn, unsigned num_args, vm_obj const * args);
+vm_obj mk_native_closure(vm_cfunction_2 fn, unsigned num_args, vm_obj const * args);
+vm_obj mk_native_closure(vm_cfunction_3 fn, unsigned num_args, vm_obj const * args);
+vm_obj mk_native_closure(vm_cfunction_4 fn, unsigned num_args, vm_obj const * args);
+vm_obj mk_native_closure(vm_cfunction_5 fn, unsigned num_args, vm_obj const * args);
+vm_obj mk_native_closure(vm_cfunction_6 fn, unsigned num_args, vm_obj const * args);
+vm_obj mk_native_closure(vm_cfunction_7 fn, unsigned num_args, vm_obj const * args);
+vm_obj mk_native_closure(vm_cfunction_8 fn, unsigned num_args, vm_obj const * args);
+vm_obj mk_native_closure(vm_cfunction_N fn, unsigned arity, unsigned num_args, vm_obj const * args);
+vm_obj mk_native_closure(vm_cfunction_1 fn, std::initializer_list<vm_obj> const & args);
+vm_obj mk_native_closure(vm_cfunction_2 fn, std::initializer_list<vm_obj> const & args);
+vm_obj mk_native_closure(vm_cfunction_3 fn, std::initializer_list<vm_obj> const & args);
+vm_obj mk_native_closure(vm_cfunction_4 fn, std::initializer_list<vm_obj> const & args);
+vm_obj mk_native_closure(vm_cfunction_5 fn, std::initializer_list<vm_obj> const & args);
+vm_obj mk_native_closure(vm_cfunction_6 fn, std::initializer_list<vm_obj> const & args);
+vm_obj mk_native_closure(vm_cfunction_7 fn, std::initializer_list<vm_obj> const & args);
+vm_obj mk_native_closure(vm_cfunction_8 fn, std::initializer_list<vm_obj> const & args);
+vm_obj mk_native_closure(vm_cfunction_N fn, unsigned arity, std::initializer_list<vm_obj> const & args);
+/* Closure to VM bytecode */
+vm_obj mk_vm_closure(unsigned fnidx, unsigned sz, vm_obj const * args);
 vm_obj mk_vm_closure(unsigned cidx, vm_obj const &);
 vm_obj mk_vm_closure(unsigned cidx, vm_obj const &, vm_obj const &);
 vm_obj mk_vm_closure(unsigned cidx, vm_obj const &, vm_obj const &, vm_obj const &);
@@ -171,6 +231,7 @@ inline vm_obj_kind kind(vm_obj_cell const * o) { return LEAN_VM_IS_PTR(o) ? o->k
 inline bool is_simple(vm_obj_cell const * o) { return !LEAN_VM_IS_PTR(o); }
 inline bool is_constructor(vm_obj_cell const * o) { return kind(o) == vm_obj_kind::Constructor; }
 inline bool is_closure(vm_obj_cell const * o) { return kind(o) == vm_obj_kind::Closure; }
+inline bool is_native_closure(vm_obj_cell const * o) { return kind(o) == vm_obj_kind::NativeClosure; }
 inline bool is_composite(vm_obj_cell const * o) { return is_constructor(o) || is_closure(o); }
 inline bool is_mpz(vm_obj_cell const * o) { return kind(o) == vm_obj_kind::MPZ; }
 inline bool is_external(vm_obj_cell const * o) { return kind(o) == vm_obj_kind::External; }
@@ -182,6 +243,7 @@ inline vm_composite * to_composite(vm_obj_cell * o) { lean_assert(is_composite(o
 inline vm_mpz * to_mpz_core(vm_obj_cell * o) { lean_assert(is_mpz(o)); return static_cast<vm_mpz*>(o); }
 inline mpz const & to_mpz(vm_obj_cell * o) { return to_mpz_core(o)->get_value(); }
 inline vm_external * to_external(vm_obj_cell * o) { lean_assert(is_external(o)); return static_cast<vm_external*>(o); }
+inline vm_native_closure * to_native_closure(vm_obj_cell * o) { lean_assert(is_native_closure(o)); return static_cast<vm_native_closure*>(o); }
 // =======================================
 
 // =======================================
@@ -206,25 +268,6 @@ class vm_state;
 /** Builtin functions that take arguments from the VM stack. */
 typedef void (*vm_function)(vm_state & s);
 
-/** Builtin functions that take arguments from the system stack.
-
-    \remark The C++ code generator produces this kind of function. */
-typedef vm_obj (*vm_cfunction)(vm_obj const &);
-typedef vm_obj (*vm_cfunction_0)();
-typedef vm_obj (*vm_cfunction_1)(vm_obj const &);
-typedef vm_obj (*vm_cfunction_2)(vm_obj const &, vm_obj const &);
-typedef vm_obj (*vm_cfunction_3)(vm_obj const &, vm_obj const &, vm_obj const &);
-typedef vm_obj (*vm_cfunction_4)(vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &);
-typedef vm_obj (*vm_cfunction_5)(vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &,
-                                 vm_obj const &);
-typedef vm_obj (*vm_cfunction_6)(vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &,
-                                 vm_obj const &, vm_obj const &);
-typedef vm_obj (*vm_cfunction_7)(vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &,
-                                 vm_obj const &, vm_obj const &, vm_obj const &);
-typedef vm_obj (*vm_cfunction_8)(vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &,
-                                 vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &);
-typedef vm_obj (*vm_cfunction_N)(unsigned n, vm_obj const *);
-
 /** Custom 'cases' operators. Given an object \c o, it returns the constructor index and stores
     the data stored in the object in the buffer \c data. */
 typedef unsigned (*vm_cases_function)(vm_obj const & o, buffer<vm_obj> & data);