From e369c3beb60270059bc7db2862782268d1d85a5d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 26 Oct 2022 07:13:40 -0700 Subject: [PATCH] fix: disallow `.` immediately after `..` Rejects the following weird example ``` ``` which was being parsed as ``` ``` --- src/Lean/Parser/Term.lean | 3 ++- tests/lean/ellipsisProjIssue.lean | 1 + tests/lean/ellipsisProjIssue.lean.expected.out | 1 + 3 files changed, 4 insertions(+), 1 deletion(-) create mode 100644 tests/lean/ellipsisProjIssue.lean create mode 100644 tests/lean/ellipsisProjIssue.lean.expected.out diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index ec695095b1..ba235199e3 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -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" >> diff --git a/tests/lean/ellipsisProjIssue.lean b/tests/lean/ellipsisProjIssue.lean new file mode 100644 index 0000000000..6312eefd60 --- /dev/null +++ b/tests/lean/ellipsisProjIssue.lean @@ -0,0 +1 @@ +#check Nat.add ...succ diff --git a/tests/lean/ellipsisProjIssue.lean.expected.out b/tests/lean/ellipsisProjIssue.lean.expected.out new file mode 100644 index 0000000000..faa0e25471 --- /dev/null +++ b/tests/lean/ellipsisProjIssue.lean.expected.out @@ -0,0 +1 @@ +ellipsisProjIssue.lean:1:17: error: unexpected `.` immediately after `..`