From ce889ddf60c52e7b3856740e3ce674b1f35436e2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 9 Nov 2014 12:55:13 -0800
Subject: [PATCH] feat(frontends/lean/scanner): disallow hierarchical names
 such as 'x.1'

---
 src/frontends/lean/scanner.cpp      | 2 +-
 tests/lean/bad_id.lean              | 5 +++++
 tests/lean/bad_id.lean.expected.out | 1 +
 3 files changed, 7 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/bad_id.lean
 create mode 100644 tests/lean/bad_id.lean.expected.out

diff --git a/src/frontends/lean/scanner.cpp b/src/frontends/lean/scanner.cpp
index 380bafb93..6f1479bc2 100644
--- a/src/frontends/lean/scanner.cpp
+++ b/src/frontends/lean/scanner.cpp
@@ -354,7 +354,7 @@ auto scanner::read_key_cmd_id() -> token_kind {
             } else if (cs[i] == '.') {
                 next_utf(cs);
                 num_utfs++;
-                if (!is_id_rest(cs, i+1))
+                if (!is_id_first(cs, i+1))
                     break;
             } else {
                 break;
diff --git a/tests/lean/bad_id.lean b/tests/lean/bad_id.lean
new file mode 100644
index 000000000..7dec22b98
--- /dev/null
+++ b/tests/lean/bad_id.lean
@@ -0,0 +1,5 @@
+import data.num
+
+definition x.y := 10
+
+definition x.1 := 10
diff --git a/tests/lean/bad_id.lean.expected.out b/tests/lean/bad_id.lean.expected.out
new file mode 100644
index 000000000..64eaa4cbd
--- /dev/null
+++ b/tests/lean/bad_id.lean.expected.out
@@ -0,0 +1 @@
+bad_id.lean:5:12: error: invalid binder, '(', '{', '[', '{{', '⦃' or identifier expected