Skip to content

Commit

Permalink
fix: do not ban .. with a . on the next line
Browse files Browse the repository at this point in the history
Without this change,
```lean
example : True := by
  refine' trivial ..
  . trivial
```
is a parse error.
  • Loading branch information
eric-wieser authored Jul 17, 2024
1 parent 1a12f63 commit 42d6124
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/Lean/Parser/Term.lean
Original file line number Diff line number Diff line change
Expand Up @@ -752,7 +752,7 @@ 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)
".." >> notFollowedBy "." "`.` immediately after `..`"
".." >> notFollowedBy (checkNoWsBefore >> ".") "`.` immediately after `..`"
def argument :=
checkWsBefore "expected space" >>
checkColGt "expected to be indented" >>
Expand Down

0 comments on commit 42d6124

Please sign in to comment.