test: for isNoncomputable

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

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