You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Triage of what … means where it is written, and how large each piece is. The reference for #1409 uses it in five ways, and the same five cover what I find elsewhere.
nothing: a matrix has a written size, and n names cannot be listed
an index set under a binder
∀ i ∈ {1, …, n}, ⋃_{i=1}^{n}
the range again
forall k in ZZ+ /\ [1; n], union(A_k, k in …)
a decimal or a continued fraction
0.333…, 1 + 1/(1 + 1/(1 + …))
a limit
nothing, and it is a different …: a limit, not a pattern
The semantics of the first four is one thing:… between shown terms names the sequence the shown terms determine, and the term after it names where it stops. So the pattern operator needs (a) a rule that reads the shown terms into a general term — an arithmetic progression from two terms (2, 4, …, 2n gives 2k), a geometric one from two (1, 2, 4, …, 2^n), a shown general term with an index (a_1, a_2, …, a_n gives a_k; x_1, …, x_n with one term shown is that too), and refusal otherwise; and (b) a context that says what to build from the general term and the bounds: a set (ZZ+ /\ [1; n] under the general term, i.e. the image of a range), a sum/product, a tuple (which is the part with no node today, #330), or a quantifier's index set. Reading a general term from three or more terms with no index shown (1, 4, 9, …) is guessing, and I would refuse it rather than pick the smallest polynomial; two terms of an arithmetic or geometric progression and a shown index are the honest cases, and they are what the books write.
Size. Small for the set, the sum/product and the binder cases: a parser rule for …/... inside a list, a reader of the progression (a hundred lines with tests), and an emitted sum(…), union(…) or range — no new node. Medium for the argument-list case, because f(x_1, …, x_n) needs a family of names of symbolic length, which is a new kind of node and touches every operation that lists children (#330's tuple design, again). Out of scope for the limit …, which is a different word spelled the same.
If the small part is wanted before v3, I can do it against the reference's rows ({1, …, n}, 1 + 2 + … + n = n(n+1)/2, ∀ i ∈ {1, …, n}); the medium part is a v3 design item next to tuples on #1019.
The small half landed in #1439 (6d3c3d9b): {1, 2, ..., n}, {2, 4, ..., 2 n}, {5, 10, 15, ...}, {..., -1, 0}, {k - 2, ..., k + 2}, 1 + 2 + ... + n, 1 * 2 * ... * n, also with …; built from ZZ /\ [a; z], a residue class cut by an interval, sum and product, with shown terms off the progression refused by name. Milestone moved to 3.0 for the larger half — the general term with an index shown and the argument list of symbolic length — which is v3's family of names (#1019).
Activity
Rafael-SOWNet commentedon Sep 21, 2026
Triage of what
…means where it is written, and how large each piece is. The reference for #1409 uses it in five ways, and the same five cover what I find elsewhere.{1, 2, …, n},{2, 4, 6, …},{…, −1, 0}ZZ+ /\ [1; n]since #1435;{ k in ZZ : k <= 0 }1 + 2 + … + n,1 · 2 · … · n,a_1 + … + a_nsum(k, k, 1, n); a sum over an indexed familysum,product(four-argument form)(x_1, …, x_n),f(x_1, …, x_n),[a_1, …, a_n]nnames cannot be listed∀ i ∈ {1, …, n},⋃_{i=1}^{n}forall k in ZZ+ /\ [1; n],union(A_k, k in …)0.333…,1 + 1/(1 + 1/(1 + …))…: a limit, not a patternThe semantics of the first four is one thing:
…between shown terms names the sequence the shown terms determine, and the term after it names where it stops. So the pattern operator needs (a) a rule that reads the shown terms into a general term — an arithmetic progression from two terms (2, 4, …, 2ngives2k), a geometric one from two (1, 2, 4, …, 2^n), a shown general term with an index (a_1, a_2, …, a_ngivesa_k;x_1, …, x_nwith one term shown is that too), and refusal otherwise; and (b) a context that says what to build from the general term and the bounds: a set (ZZ+ /\ [1; n]under the general term, i.e. the image of a range), asum/product, a tuple (which is the part with no node today, #330), or a quantifier's index set. Reading a general term from three or more terms with no index shown (1, 4, 9, …) is guessing, and I would refuse it rather than pick the smallest polynomial; two terms of an arithmetic or geometric progression and a shown index are the honest cases, and they are what the books write.Size. Small for the set, the sum/product and the binder cases: a parser rule for
…/...inside a list, a reader of the progression (a hundred lines with tests), and an emittedsum(…),union(…)or range — no new node. Medium for the argument-list case, becausef(x_1, …, x_n)needs a family of names of symbolic length, which is a new kind of node and touches every operation that lists children (#330's tuple design, again). Out of scope for the limit…, which is a different word spelled the same.If the small part is wanted before v3, I can do it against the reference's rows (
{1, …, n},1 + 2 + … + n = n(n+1)/2,∀ i ∈ {1, …, n}); the medium part is a v3 design item next to tuples on #1019.Happypig375 commentedon Sep 21, 2026
Seems alright. The small case probably fits in 2.8, the medium case can be designed together with v3 together with symbolic length nodes.
Happypig375 commentedon Sep 21, 2026
I put this in 2.8. When the first part is done reassign milestone.
... is the pattern operator: the progression the shown terms determin…
Rafael-SOWNet commentedon Sep 21, 2026
The small half landed in #1439 (
6d3c3d9b):{1, 2, ..., n},{2, 4, ..., 2 n},{5, 10, 15, ...},{..., -1, 0},{k - 2, ..., k + 2},1 + 2 + ... + n,1 * 2 * ... * n, also with…; built fromZZ /\ [a; z], a residue class cut by an interval,sumandproduct, with shown terms off the progression refused by name. Milestone moved to 3.0 for the larger half — the general term with an index shown and the argument list of symbolic length — which is v3's family of names (#1019).