max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: disallow . immediately after ..

Browse source 
Rejects the following weird example
```
```
which was being parsed as
```
```
This commit is contained in:
Leonardo de Moura 2022-10-26 07:13:40 -07:00
parent d7e732e886
commit e369c3beb6
3 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Lean/Parser/Term.lean
View file

@ -547,7 +547,8 @@ We use them to implement `macro_rules` and `elab_rules`
def namedArgument := leading_parser (withAnonymousAntiquot := false)
atomic ("(" >> ident >> " := ") >> withoutPosition termParser >> ")"
def ellipsis := leading_parser (withAnonymousAntiquot := false) ".."
def ellipsis := leading_parser (withAnonymousAntiquot := false)
".." >> notFollowedBy "." "`.` immediately after `..`"
def argument :=
checkWsBefore "expected space" >>
checkColGt "expected to be indented" >>

1
tests/lean/ellipsisProjIssue.lean Normal file
View file

@ -0,0 +1 @@
#check Nat.add ...succ

1
tests/lean/ellipsisProjIssue.lean.expected.out Normal file
View file

@ -0,0 +1 @@
ellipsisProjIssue.lean:1:17: error: unexpected `.` immediately after `..`