Skip to content

| is divisibility, and was disjunction - #1241

Merged
Rafael-SOWNet merged 1 commit into
masterfrom
bar-is-divides
Sep 10, 2026
Merged

Rafael-SOWNet merged 1 commit into
masterfrom
bar-is-divides

Conversation

@Rafael-SOWNet

Copy link
Copy Markdown
Member

Implements your decision on #1212:

Just make | divides; semantic versioning allows such a breakage and the break should be put earlier in the breakages list.

Both halves done — the change is direct, and the entry is first in BREAKING-CHANGES.md's unreleased section rather than in its place in filing order.

a | b is now the statement that b is a whole multiple of a — the same node a divides b has built since #1220, at the same precedence. Defined over the integers and NaN over anything else, the way an inequality is over a non-real number. 0 | 0 is True; 0 | b is otherwise False.

What moves

Was Is
"2 | 6" 2 or 6, a disjunction of two numbers 2 divides 6, which evaluates True
"x > 0 | x < -1" x > 0 or x < -1 regrouped — divisibility binds tighter than a comparison
"A | B" on booleans A or B NaN, since divisibility is a statement about integers
"{ x | x > 0 }" one-element FiniteSet of x or x > 0 one-element FiniteSet of (x divides x) > 0

It is a silent change: input that used | still parses and answers something else. That is what I wanted the two-release migration for, and your call was that a breaking-changes row is the right protection. Recorded plainly at the top of the section rather than softened.

What it cost, measured

7 of 8,525 tests referenced the old reading: five boolean-solver inputs written A | B, and two written to record this spelling as at risk in the first place.

The reason it is that small is the reason to expect it: or is the primary spelling and is what the library prints, so a round-tripped expression never held a |. Replacing | with or restores the old reading exactly, everywhere.

I had argued this was too risky to do in one step. My argument was about the shape of the risk and I had not measured its size; the size is seven tests.

Mechanics

Grammar regenerated with ANTLR and put through the post-processor, with the parser confirmed internal again by counting rather than by assuming — that step silently does nothing if the library does not compile, so it is worth checking.

Syntax.md's precedence table moves | from level 3 beside or to level 8 beside in and divides.

Checked

All five suites: UnitTests 8,514 and 1,500, FSharpWrapperUnitTests 134, InteractiveWrapperUnitTests 18, TerminalUnitTests 41.

Item 6 of #1019 is updated with what this actually cost.

🤖 Generated with Claude Code

https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura

`|` was the one spelling in the grammar that already means something else in
mathematics than we read it as: it is divides (a | b), "such that" ({x | P(x)}),
"given" (P(A | B)), and the delimiter in |x|. None of those is disjunction,
which is written with a vee. So input written by a mathematician was read as an
or and answered as one.

a | b is now the statement that b is a whole multiple of a -- the same node
a divides b has built since #1220, at the same precedence. Defined over the
integers and NaN over anything else, the way an inequality is over a non-real
number. 0 | 0 is True; 0 | b is otherwise False.

This is a silent change: an expression that used | still parses and answers
something else. I proposed a two-release migration through a parse error to
avoid that; Happypig375's decision on #1212 was to make the change directly,
since semantic versioning admits it, and to put the entry early in the
breakages list. Both done.

    "2 | 6"              was  2 or 6                   is  2 divides 6, True
    "x > 0 | x < -1"     was  a disjunction            is  regrouped, since
                                                           divisibility binds
                                                           tighter than >
    "A | B" on booleans  was  A or B                   is  NaN

or is unaffected and always was the primary spelling -- it is what the library
prints, so a round-tripped expression never held a | to begin with. Replacing |
with or restores the old reading exactly, everywhere. That is why the cost is
small: 7 of 8,525 tests referenced the old reading, five of them boolean-solver
inputs written A | B and two written to record this spelling as at risk.

The grammar is regenerated and post-processed; the parser is internal again,
checked rather than assumed.

All five suites green: UnitTests 8514 and 1500, FSharpWrapperUnitTests 134,
InteractiveWrapperUnitTests 18, TerminalUnitTests 41.

#1212

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura
@Happypig375

Happypig375 commented Sep 10, 2026 •

Copy link
Copy Markdown
Member

it may also be consistent to retire &'s meaning of "and" so that it can be used instead as a potential UnicodeMath operator (#1242) (do we "want" to follow through with those semantics? or consistency between "and" and "or" id enough?)

@Rafael-SOWNet

Copy link
Copy Markdown
Member Author

I would keep &, and I think the decision belongs to #1242's entry-point question rather than to this one.

What & actually is in UnicodeMath, checked in UTN #28 §3.19 rather than from memory:

█(10&x+&3&y=2@3&x+&13&y=4) … the meaning of the ampersands alternate between align and spacer, with an implied spacer at the start of the line. So every odd & is an alignment point and every even & is a place where space may be added to align the equations. This convention is used in AmSTeX.

So it is a layout marker inside an equation array delimited by █( … ), alternating align/spacer. It is not a binary operator on propositions, and it only occurs inside a bracketed construct we do not have.

That is why it is not the same case as |. The reason | had to go was not that it was a programming convention — it was that a | b at expression level already means something to a mathematician: divides, "such that", "given". Well-formed input written by someone who knows the mathematics was silently answered as a disjunction. That is a correctness problem.

a & b is not misread by anyone. & is absent from mathematical notation rather than taken by it — conjunction is ∧ — so there is no reading it competes with in the position it occupies. Consistency between and and or is an aesthetic argument, and it was not the argument for |.

And #1242 already contains the resolution, in your own words: "UnicodeMath parsing and output may be a separate entry point". If it is, the question dissolves — & is an alignment marker there and conjunction in the ASCII grammar, and neither sees the other. The choice is only forced if UnicodeMath is parsed by the same entry point.

So my answer to "do we want to follow through with those semantics, or is consistency enough?" is: consistency is enough, and it is already satisfied — and/or are the primary spellings and are what we print.

What would change my mind, and I would rather say it now than re-litigate later: if #1242 lands as one grammar rather than two, then & inside an equation array does collide and should go with |.

Cost, if you decide otherwise: identical in shape to | and about as small. Andf prints as and, never &, so a round-tripped expression never contains one; the exposure is 29 test inputs, against the 7 that | cost. I am happy to do it — it is an hour — I just do not think there is a reason yet.

@Rafael-SOWNet
Rafael-SOWNet merged commit f6798c6 into master Sep 10, 2026
32 checks passed
@Rafael-SOWNet
Rafael-SOWNet deleted the bar-is-divides branch September 10, 2026 06:04
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