Skip to content

Modal syntax update + cubical interval - #74

Merged
fizruk merged 4 commits into
rzk-lang:mainfrom
LIshy2:main
Jul 21, 2026
Merged

Modal syntax update + cubical interval#74
fizruk merged 4 commits into
rzk-lang:mainfrom
LIshy2:main

Conversation

@LIshy2

@LIshy2 LIshy2 commented Jun 5, 2026

Copy link
Copy Markdown
Contributor

No description provided.

fizruk added a commit that referenced this pull request Jul 21, 2026
The bracketing rule dates from the first modal-syntax PR; the modal
syntax has since moved on (see #74), so the old spelling should not
read as highlighted syntax. The tags and let mod/mod keywords are
untouched.
Snapshots regenerated over the merged grammar. One overlap resolved
against the incoming side: the operator catcher keeps | (since #319
a bare | separates match branches and #data constructors), while <
stays dropped as this PR intends (nothing bare-< remains in the
syntax).
@fizruk

fizruk commented Jul 21, 2026

Copy link
Copy Markdown
Member

I have merged main into this branch to resolve the conflicts with the v0.11.0 grammar update (#78) and regenerated the snapshots. Everything from this PR survives as intended: the interval cube 𝕀 / II and its endpoints, the :♭-style modality annotations, and the removal of < from the operator catch-all.

One overlap I resolved in favour of main: the operator catch-all keeps |. Since rzk v0.11.0 a bare | separates match branches and #data constructors, so it should stay styled as an operator.

@fizruk
fizruk merged commit 3539890 into rzk-lang:main Jul 21, 2026
1 check passed
@fizruk fizruk mentioned this pull request Jul 21, 2026
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.

2 participants