From 373a64ee09678d03db5eb27457ec4c2ae909abea Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 16 Feb 2022 13:37:49 -0800 Subject: [PATCH] test: for `isNoncomputable` --- tests/lean/isNoncomputable.lean | 16 ++++++++++++++++ tests/lean/isNoncomputable.lean.expected.out | 4 ++++ 2 files changed, 20 insertions(+) create mode 100644 tests/lean/isNoncomputable.lean create mode 100644 tests/lean/isNoncomputable.lean.expected.out 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