From 74be3031b1b0813c6ec54cfce4e9bdabe57b40d9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 29 Jul 2015 08:14:39 -0700
Subject: [PATCH] feat(frontends/lean/decl_cmds): sign an error if
 "noncomputable" keyword is used in the HoTT library or with non-definitions

---
 src/frontends/lean/decl_cmds.cpp           | 4 ++++
 tests/lean/noncomp_hott.hlean              | 1 +
 tests/lean/noncomp_hott.hlean.expected.out | 1 +
 tests/lean/noncomp_thm.lean                | 1 +
 tests/lean/noncomp_thm.lean.expected.out   | 1 +
 5 files changed, 8 insertions(+)
 create mode 100644 tests/lean/noncomp_hott.hlean
 create mode 100644 tests/lean/noncomp_hott.hlean.expected.out
 create mode 100644 tests/lean/noncomp_thm.lean
 create mode 100644 tests/lean/noncomp_thm.lean.expected.out

diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index af3bb7cda..9fe4aab49 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -1070,6 +1070,10 @@ public:
         m_is_private(is_private), m_is_protected(is_protected), m_is_noncomputable(is_noncomputable),
         m_pos(p.pos()), m_attributes(kind == Abbreviation || kind == LocalAbbreviation) {
         lean_assert(!(m_is_private && m_is_protected));
+        if (!is_standard(m_p.env()) && is_noncomputable)
+            throw exception("invalid 'noncomputable' declarations, it can only be used in the standard library");
+        if (kind != Definition && is_noncomputable)
+            throw exception("invalid 'noncomputable' declaration, it can only be used for definitions");
     }
 
     environment operator()() {
diff --git a/tests/lean/noncomp_hott.hlean b/tests/lean/noncomp_hott.hlean
new file mode 100644
index 000000000..0a59b906b
--- /dev/null
+++ b/tests/lean/noncomp_hott.hlean
@@ -0,0 +1 @@
+noncomputable definition foo := 10
diff --git a/tests/lean/noncomp_hott.hlean.expected.out b/tests/lean/noncomp_hott.hlean.expected.out
new file mode 100644
index 000000000..ac5ec6f74
--- /dev/null
+++ b/tests/lean/noncomp_hott.hlean.expected.out
@@ -0,0 +1 @@
+noncomp_hott.hlean:1:0: error: invalid 'noncomputable' declarations, it can only be used in the standard library
diff --git a/tests/lean/noncomp_thm.lean b/tests/lean/noncomp_thm.lean
new file mode 100644
index 000000000..d31bf82c7
--- /dev/null
+++ b/tests/lean/noncomp_thm.lean
@@ -0,0 +1 @@
+noncomputable theorem foo : true := trivial
diff --git a/tests/lean/noncomp_thm.lean.expected.out b/tests/lean/noncomp_thm.lean.expected.out
new file mode 100644
index 000000000..0caaeeb69
--- /dev/null
+++ b/tests/lean/noncomp_thm.lean.expected.out
@@ -0,0 +1 @@
+noncomp_thm.lean:1:0: error: invalid 'noncomputable' declaration, it can only be used for definitions