Il 08/11/19 12:32, Mario Carneiro ha scritto:> This came up for me with
"mixfix" operators. With MM0 currently, you can
define "a + b", but you can't write "a +g[ G ] b" representing a general
group addition, because the +g notation does not begin with a constant.
But it can be analyzed essentially like any other infix notation: it is
marked either left or right assoc, and the inner variables are treated
like they would be in a general notation.
That seems to be a good idea to me: the difficulty of infix operators is
that you have to allow to begin parsing the first variable of a
production without yet knowing that the production is (and therefore
what is its precedence). But once you find the first constant (suppose
to be discriminating) you know which production is, and you just have to
call recursively the parser for each of the other constants. So
supporting a postfix operator or a more general "mixfix" operator
shouldn't add a big marginal work, while it would unlock a few notations
that it is nice to have in mathematics.
Basically this is also how the ternary operator in C works, at the level
of parsing.
Giovanni.
--
Giovanni Mascellani <[email protected]>
Postdoc researcher - Université Libre de Bruxelles
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/bd4d08b5-0b61-6861-ffc8-f56d1ad99f93%40gmail.com.
