diff --git a/library/init/data/uint.lean b/library/init/data/uint.lean
index 990bbaca05..76135d461b 100644
--- a/library/init/data/uint.lean
+++ b/library/init/data/uint.lean
@@ -21,14 +21,12 @@ def uint8.add (a b : uint8) : uint8 := ⟨a.val + b.val⟩
 def uint8.sub (a b : uint8) : uint8 := ⟨a.val - b.val⟩
 @[extern cpp inline "#1 * #2"]
 def uint8.mul (a b : uint8) : uint8 := ⟨a.val * b.val⟩
-@[extern cpp inline "#1 == 0 ? 0 : #1 / #2"]
+@[extern cpp inline "#2 == 0 ? 0 : #1 / #2"]
 def uint8.div (a b : uint8) : uint8 := ⟨a.val / b.val⟩
-@[extern cpp inline "#1 == 0 ? 0 : #1 % #2"]
+@[extern cpp inline "#2 == 0 ? 0 : #1 % #2"]
 def uint8.mod (a b : uint8) : uint8 := ⟨a.val % b.val⟩
 def uint8.modn (a : uint8) (n : nat) : uint8 := ⟨a.val %ₙ n⟩
-@[extern cpp inline "#1 < #2"]
 def uint8.lt (a b : uint8) : Prop := a.val < b.val
-@[extern cpp inline "#1 <= #2"]
 def uint8.le (a b : uint8) : Prop := a.val ≤ b.val
 
 instance : has_zero uint8     := ⟨uint8.of_nat 0⟩
@@ -43,14 +41,17 @@ instance : has_lt uint8       := ⟨uint8.lt⟩
 instance : has_le uint8       := ⟨uint8.le⟩
 instance : inhabited uint8    := ⟨0⟩
 
+@[extern cpp inline "#1 == #2"]
 def uint8.dec_eq (a b : uint8) : decidable (a = b) :=
 uint8.cases_on a $ λ n, uint8.cases_on b $ λ m,
   if h : n = m then is_true (h ▸ rfl) else is_false (λ h', uint8.no_confusion h' (λ h', absurd h' h))
 
+@[extern cpp inline "#1 < #2"]
 def uint8.dec_lt (a b : uint8) : decidable (a < b) :=
 uint8.cases_on a $ λ n, uint8.cases_on b $ λ m,
   infer_instance_as (decidable (n < m))
 
+@[extern cpp inline "#1 <= #2"]
 def uint8.dec_le (a b : uint8) : decidable (a ≤ b) :=
 uint8.cases_on a $ λ n, uint8.cases_on b $ λ m,
   infer_instance_as (decidable (n <= m))
diff --git a/src/library/compiler/emit_cpp.cpp b/src/library/compiler/emit_cpp.cpp
index 8da5e9d05a..a75718c81f 100644
--- a/src/library/compiler/emit_cpp.cpp
+++ b/src/library/compiler/emit_cpp.cpp
@@ -17,6 +17,7 @@ Author: Leonardo de Moura
 #include "library/compiler/llnf_code.h"
 #include "library/compiler/builtin.h"
 #include "library/compiler/export_attribute.h"
+#include "library/compiler/extern_attribute.h"
 
 namespace lean {
 static std::string to_cpp_type(expr const & e) {
@@ -273,6 +274,7 @@ static char const * get_scalar_type_from_size(unsigned i) {
 
 struct emit_fn_fn {
     std::ostream &  m_out;
+    name            m_cpp{"cpp"};
     name_generator  m_ngen;
     environment     m_env;
     local_ctx       m_lctx;
@@ -289,8 +291,12 @@ struct emit_fn_fn {
         return m_lctx.get_local_decl(x).get_type() == mk_enf_object_type();
     }
 
+    void emit_unit(std::ostream & out) {
+        out << "lean::box(0)";
+    }
+
     void emit_unit() {
-        m_out << "lean::box(0)";
+        emit_unit(m_out);
     }
 
     void emit_constant(expr const & c) {
@@ -304,11 +310,15 @@ struct emit_fn_fn {
             m_out << to_cpp_name(m_env, const_name(c));
     }
 
-    void emit_fvar(expr const & x) {
+    void emit_fvar(std::ostream & out, expr const & x) {
         lean_assert(is_fvar(x));
         name const & id = fvar_name(x);
         lean_assert(id.is_numeral());
-        m_out << "x_" << id.get_numeral();
+        out << "x_" << id.get_numeral();
+    }
+
+    void emit_fvar(expr const & x) {
+        emit_fvar(m_out, x);
     }
 
     void emit_lbl(expr const & jp) {
@@ -360,11 +370,15 @@ struct emit_fn_fn {
         m_out << ";\n";
     }
 
-    void emit_arg(expr const & arg) {
+    void emit_arg(std::ostream & out, expr const & arg) {
         if (is_fvar(arg))
-            emit_fvar(arg);
+            emit_fvar(out, arg);
         else
-            emit_unit();
+            emit_unit(out);
+    }
+
+    void emit_arg(expr const & arg) {
+        emit_arg(m_out, arg);
     }
 
     void emit_args(unsigned sz, expr const * args) {
@@ -374,6 +388,12 @@ struct emit_fn_fn {
         }
     }
 
+    string_ref arg_to_string_ref(expr const & arg) {
+        std::ostringstream out;
+        emit_arg(out, arg);
+        return string_ref(out.str());
+    }
+
     void emit_apply(expr const & x, buffer<expr> const & args) {
         lean_assert(args.size() > 0);
         expr const & f = args[0];
@@ -543,21 +563,16 @@ struct emit_fn_fn {
         m_out << ");\n";
     }
 
-    void emit_native_constant(expr const &x, expr const &fn, buffer<expr> const &args) {
-        buffer<bool> used_args;
-        lean_verify(get_native_used_args(m_env, const_name(fn), used_args));
-        lean_assert(used_args.size() == args.size());
+    void emit_native_constant(expr const & x, expr const & fn, buffer<expr> const & args) {
         emit_lhs(x);
-        emit_constant(fn);
-        m_out << "(";
-        bool first = true;
-        for (unsigned i = 0; i < args.size(); i++) {
-            if (used_args[i]) {
-                if (first) first = false; else m_out << ", ";
-                emit_arg(args[i]);
-            }
+        string_refs arg_strs;
+        unsigned i = args.size();
+        while (i > 0) {
+            --i;
+            arg_strs = string_refs(arg_to_string_ref(args[i]), arg_strs);
         }
-        m_out << ");\n";
+        emit_extern_call(m_out, m_env, m_cpp, const_name(fn), arg_strs);
+        m_out << ";\n";
     }
 
     void emit_instr(local_decl const & d) {
diff --git a/src/library/compiler/extern_attribute.cpp b/src/library/compiler/extern_attribute.cpp
index 51d79df5bb..6dc783e6fd 100644
--- a/src/library/compiler/extern_attribute.cpp
+++ b/src/library/compiler/extern_attribute.cpp
@@ -8,6 +8,9 @@ Authors: Leonardo de Moura
 #include "util/object_ref.h"
 #include "library/util.h"
 #include "library/attribute_manager.h"
+#include "library/compiler/builtin.h" // TODO(Leo): delete
+
+void initialize_init_lean_extern();
 
 namespace lean {
 object* mk_adhoc_ext_entry_core(object*);
@@ -16,6 +19,7 @@ object* mk_std_ext_entry_core(object*, object*);
 object* mk_foreign_ext_entry_core(object*, object*);
 object* mk_extern_call_core(object*, object*, object*);
 object* mk_extern_attr_data_core(object*, object*);
+object* mk_extern_call_core(object*, object*, object*);
 
 typedef object_ref extern_entry;
 typedef list_ref<extern_entry> extern_entries;
@@ -113,7 +117,39 @@ extern_attr const & get_extern_attr() {
     return static_cast<extern_attr const &>(get_system_attribute("extern"));
 }
 
+bool emit_extern_call_core(std::ostream & out, environment const & env, name const & backend, name const & fn, string_refs const & attrs) {
+    if (std::shared_ptr<extern_attr_data> const & data = get_extern_attr().get(env, fn)) {
+        extern_attr_data_value const & v = data->m_value;
+        inc(v.raw()); inc(backend.raw()); inc(attrs.raw());
+        object * r = mk_extern_call_core(v.raw(), backend.raw(), attrs.raw());
+        if (is_scalar(r)) return false;
+        object * s = cnstr_get(r, 0);
+        out << string_cstr(s);
+        dec(r);
+        return true;
+    } else {
+        return false;
+    }
+}
+
+void emit_extern_call(std::ostream & out, environment const & env, name const & backend, name const & fn, string_refs const & attrs) {
+    if (emit_extern_call_core(out, env, backend, fn, attrs))
+        return;
+    /* TODO(Leo): delete the following backward compatibility code */
+    name _fn = *get_native_constant_cname(env, fn);
+    out << _fn << "(";
+    bool first = true;
+    string_refs it = attrs;
+    while (!empty(it)) {
+        if (first) first = false; else out << ", ";
+        out << string_cstr(head(it).raw());
+        it = tail(it);
+    }
+    out << ")";
+}
+
 void initialize_extern_attribute() {
+    initialize_init_lean_extern(); // Lean module initialization
     register_system_attribute(extern_attr("extern", "builtin and foreign functions",
                                           [](environment const & env, io_state const &, name const &, unsigned, bool persistent) {
                                               if (!persistent) throw exception("invalid [extern] attribute, it must be persistent");
diff --git a/src/library/compiler/extern_attribute.h b/src/library/compiler/extern_attribute.h
index 636a68536b..081fead235 100644
--- a/src/library/compiler/extern_attribute.h
+++ b/src/library/compiler/extern_attribute.h
@@ -7,7 +7,8 @@ Authors: Leonardo de Moura
 #pragma once
 #include "kernel/environment.h"
 namespace lean {
-string_ref mk_extern_call(environment const & env, string_ref const & backend, string_refs const & attrs);
+bool emit_extern_call_core(std::ostream & out, environment const & env, name const & backend, name const & fn, string_refs const & attrs);
+void emit_extern_call(std::ostream & out, environment const & env, name const & backend, name const & fn, string_refs const & attrs);
 void initialize_extern_attribute();
 void finalize_extern_attribute();
 }