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