Validation of atoms should ignore whitespace #6011
Labels
bug
Something isn't working
Comments
david-christiansen
added a commit
to david-christiansen/lean4
that referenced
this issue
Nov 8, 2024
github-merge-queue bot
pushed a commit
that referenced
this issue
Nov 14, 2024
This PR improves the validation of new syntactic tokens. Previously, the validation code had inconsistencies: some atoms would be accepted only if they had a leading space as a pretty printer hint. Additionally, atoms with internal whitespace are no longer allowed. Closes #6011
JovanGerb
pushed a commit
to JovanGerb/lean4
that referenced
this issue
Jan 21, 2025
…r#6012) This PR improves the validation of new syntactic tokens. Previously, the validation code had inconsistencies: some atoms would be accepted only if they had a leading space as a pretty printer hint. Additionally, atoms with internal whitespace are no longer allowed. Closes leanprover#6011
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Description
New atoms introduced by
syntaxand its derived commands are not allowed to begin with digits or single or double quotes, nor may their first two characters be a valid prefix of an escaped name. They may also not be empty.We surround atoms with spaces to indicate pretty-printing, but the atom validation routine does not ignore these spaces.
Context
This came up while documenting the specific rules for infix operators in the reference manual.
Steps to Reproduce
infix:40 "9" => Nat.addinvalid atominfix:40 " 9" => Nat.addExpected behavior:
The error messages should be identical. An invalid atom doesn't become valid because it should be printed with spaces.
Actual behavior:
The declaration is accepted.
Versions
From
live.lean-lang.org:"4.15.0-nightly-2024-11-08"Additional Information
Link to code
Impact
Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.
The text was updated successfully, but these errors were encountered: