feat(frontends/lean/scanner): disallow hierarchical names such as 'x.1'
This commit is contained in:
parent
df5a17cdce
commit
ce889ddf60
3 changed files with 7 additions and 1 deletions
|
@ -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;
|
||||
|
|
5
tests/lean/bad_id.lean
Normal file
5
tests/lean/bad_id.lean
Normal file
|
@ -0,0 +1,5 @@
|
|||
import data.num
|
||||
|
||||
definition x.y := 10
|
||||
|
||||
definition x.1 := 10
|
1
tests/lean/bad_id.lean.expected.out
Normal file
1
tests/lean/bad_id.lean.expected.out
Normal file
|
@ -0,0 +1 @@
|
|||
bad_id.lean:5:12: error: invalid binder, '(', '{', '[', '{{', '⦃' or identifier expected
|
Loading…
Reference in a new issue