diff --git a/library/data/real/complete.lean b/library/data/real/complete.lean
index 2bff36f60..45b31c62a 100644
--- a/library/data/real/complete.lean
+++ b/library/data/real/complete.lean
@@ -218,7 +218,7 @@ theorem rewrite_helper10 (a b c d : ℝ) : c - d = (c - a) + (a - b) + (b - d) :
 
 noncomputable definition rep (x : ℝ) : s.reg_seq := some (quot.exists_rep x)
 
-noncomputable definition re_abs (x : ℝ) : ℝ :=
+definition re_abs (x : ℝ) : ℝ :=
   quot.lift_on x (λ a, quot.mk (s.r_abs a)) (take a b Hab, quot.sound (s.r_abs_well_defined Hab))
 
 theorem r_abs_nonneg {x : ℝ} : zero ≤ x → re_abs x = x :=
diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index 9fe4aab49..b0c57af82 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -873,9 +873,13 @@ class definition_cmd_fn {
                     throw exception(sstream() << "definition '" << n << "' was marked as noncomputable because '" << *reason
                                     << "' is still in theorem queue (solution: use command 'reveal " << *reason << "'");
                 } else {
-                    throw exception(sstream() << "definition '" << n << "' is noncomputable, it depends on '" << *reason << "'");
+                    throw exception(sstream() << "definition '" << n
+                                    << "' is noncomputable, it depends on '" << *reason << "'");
                 }
             }
+            if (m_is_noncomputable && !is_marked_noncomputable(m_env, real_n)) {
+                throw exception(sstream() << "definition '" << n << "' was incorrectly marked as noncomputable");
+            }
             // TODO(Leo): register aux_decls
             if (!m_is_private)
                 m_p.add_decl_index(real_n, m_pos, m_p.get_cmd_token(), type);
diff --git a/tests/lean/noncomp_error.lean b/tests/lean/noncomp_error.lean
new file mode 100644
index 000000000..8f49f6777
--- /dev/null
+++ b/tests/lean/noncomp_error.lean
@@ -0,0 +1 @@
+noncomputable definition a := 2
diff --git a/tests/lean/noncomp_error.lean.expected.out b/tests/lean/noncomp_error.lean.expected.out
new file mode 100644
index 000000000..15d3c3dd0
--- /dev/null
+++ b/tests/lean/noncomp_error.lean.expected.out
@@ -0,0 +1 @@
+noncomp_error.lean:1:0: error: definition 'a' was incorrectly marked as noncomputable