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
@chenson2018 chenson2018 self-assigned this Jul 5, 2026

@chenson2018 chenson2018 left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

@chenson2018 chenson2018 added this pull request to the merge queue Jul 5, 2026
@github-merge-queue github-merge-queue Bot removed this pull request from the merge queue due to a conflict with the base branch Jul 5, 2026
@VitaliPath VitaliPath force-pushed the fix/well-formed-notation-collision branch from c9b0b48 to 6b01f2b Compare July 5, 2026 17:43
@VitaliPath

VitaliPath commented Jul 5, 2026

Copy link
Copy Markdown
Author

Hey @chenson2018, I just rebased to resolve the import conflict. The history is clean, and the CI checks are green again. Ready for the merge queue whenever you have a moment

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