Skip to content

fix(Foundations): add noWs guard to well-formed postfix notation#675

Open
VitaliPath wants to merge 2 commits into
leanprover:mainfrom
VitaliPath:fix/well-formed-notation-collision
Open

fix(Foundations): add noWs guard to well-formed postfix notation#675
VitaliPath wants to merge 2 commits into
leanprover:mainfrom
VitaliPath:fix/well-formed-notation-collision

Conversation

@VitaliPath

Copy link
Copy Markdown

Addresses #638. Converts the global well-formed notation to a macro with a noWs whitespace guard. This explicitly prevents the postfix parser from greedily consuming the token across line breaks, resolving the syntax collision with TimeM's prefix tick notation when both modules are imported simultaneously.

@chenson2018

Copy link
Copy Markdown
Collaborator

Could you please add a test in CSLibTests for this?

@VitaliPath

Copy link
Copy Markdown
Author

Added the regression test in CslibTests/HasWellFormed.lean and verified the fix resolves both the prefix syntax collision and preserves the expected postfix evaluation. Let me know if you need anything else.

@VitaliPath VitaliPath force-pushed the fix/well-formed-notation-collision branch from 7c59e3e to c045387 Compare June 22, 2026 22:50
@VitaliPath

Copy link
Copy Markdown
Author

Added the #guard_msgs wrapper to the test to prevent the compiler info trace from failing the strict CI checks. Should be totally green now

@VitaliPath VitaliPath force-pushed the fix/well-formed-notation-collision branch from c045387 to c9b0b48 Compare June 22, 2026 22:58
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants