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
Neither Mathematica nor SymPy has the existence and universal quantifiers. It would be nice to have them, for example, like that: exists x in R and x < 3 so x ^ 2 = 4
and forall x in C exists y in P such Im(x) = y
Measured on master at a45a7256: genuinely unimplemented. Every spelling I tried is a parse error:
exists x in RR so x^2 = 4 -> UnhandledParseException
forall x in RR, x^2 >= 0 -> UnhandledParseException
exists(x, x^2 = 4) -> UnhandledParseException
Recording it so the issue carries a date rather than an assumption, since a third of the ones I re-measured this week turned out to have been delivered without the checklist noticing.
The blocker is shared with #248 (Σ, Π) and with #495's syntax half: all three need the grammar to bind a variable — exists x in S, sum(i, …), a => … are the same construct wearing different clothes — and there is no binder in the parser today. ConditionalSet binds one ({ x : p(x) }), so the entity side has the concept; the parser does not generalise it.
Whichever of the three is built first pays for that machinery and the other two become much cheaper, which seems worth knowing before any of them is scheduled.
Activity
Rafael-SOWNet commentedon Aug 16, 2026
Measured on
masterata45a7256: genuinely unimplemented. Every spelling I tried is a parse error:Recording it so the issue carries a date rather than an assumption, since a third of the ones I re-measured this week turned out to have been delivered without the checklist noticing.
The blocker is shared with #248 (Σ, Π) and with #495's syntax half: all three need the grammar to bind a variable —
exists x in S,sum(i, …),a => …are the same construct wearing different clothes — and there is no binder in the parser today.ConditionalSetbinds one ({ x : p(x) }), so the entity side has the concept; the parser does not generalise it.Whichever of the three is built first pays for that machinery and the other two become much cheaper, which seems worth knowing before any of them is scheduled.
forall, exists and exists! are quantified statements over a mandatory…
Rafael-SOWNet commentedon Sep 29, 2026
Delivered by #1421. The body follows
:rather thansoorsuch, as in a set builder. The two examples here, on master at dd72825:exists!,∀,∃and∃!are there too. Moved to 2.6.0, which ships it.