Open janvrany opened 7 months ago
Yeah it's a mess.
So there is one package, Z3, that is "leaf" in that it must NOT depend on anything. That was the easy part. The hard part, IIRC, was PreSmalltalks. Shall it use Unicode selectors, or not? I vaguely remember there were problems with either way.
Then there was ∃. That's not a selector, that's new block syntax, e.g. Archimedes Axiom is written [ ∀x ∃y | y>x ]
. I suggest we leave that alone for now. There are no acual users of it right now anyway (Refinements and Sprite create instances of ForAll
and Exists
explicitly).
Long time ago the idea if package MathNotation was to provide "syntactic sugar" by providing "fancy" selectors like ∃ or ∈ to allow nice math expressions. However, this never really worked dependency-wise and been abandoned long time ago.
So perhaps it is time to move all this "fancy math" extensions to their respective packages and make MathNotation package to only provide support for these in compiler (parser)