Commit 2026-11-10 11:56 b7a8e3a8

chore(Algebra/Polynomial): parse R[X] as R + [ + X + ] (#45573) The current notation has several issues:

1. It accepts whitespace, so R [X] parses as Polynomial R too.
2. It makes [X] a token, so simp [X] parses as simp + [X] (a parse error) rather than the expected simp + [ + X + ] because of the longest parse rule. Replacing the notation containing the [X] token by a syntax containing the [, X, ] tokens separated by noWs fixes the second issue. Adding one more noWs before the [ token fixes the first issue. The priority of the syntax is decided in comparison to that of AddMonoidAlgebra (which is high) and GetElem. Written by Claude Opus, tweaked by myself. Assisted-by: Claude Opus 5.5