diff --git a/tests/lean/isNoncomputable.lean b/tests/lean/isNoncomputable.lean
new file mode 100644
index 0000000000..856d8a40e3
--- /dev/null
+++ b/tests/lean/isNoncomputable.lean
@@ -0,0 +1,16 @@
+import Lean
+open Lean
+
+def test (declName : Name) : MetaM Unit := do
+  if isNoncomputable (← getEnv) declName then
+    IO.println s!"{declName} is marked as noncomputable"
+  else
+    IO.println s!"{declName} is not marked as noncomputable"
+
+noncomputable def foo (x : Nat) : Nat :=
+  x + Classical.ofNonempty
+
+#eval test ``List.map
+#eval test ``foo
+#eval test ``Classical.ofNonempty
+#eval test ``Array.map
diff --git a/tests/lean/isNoncomputable.lean.expected.out b/tests/lean/isNoncomputable.lean.expected.out
new file mode 100644
index 0000000000..e92f232806
--- /dev/null
+++ b/tests/lean/isNoncomputable.lean.expected.out
@@ -0,0 +1,4 @@
+List.map is not marked as noncomputable
+foo is marked as noncomputable
+Classical.ofNonempty is marked as noncomputable
+Array.map is not marked as noncomputable