Re: [isabelle] Isabelle operator precedence
On Fri, 9 Nov 2012, Tobias Nipkow wrote:
Am 06/11/2012 03:11, schrieb Christian Sternagel:
Again, when both arguments have the same precedence it means that the operator
is non-associative, try, e.g., to enter
term "x ≠ x ≠ y"
(Note that this only works with the xsymbol for not-equal, since the ASCII
symbol ~= is declared as "infixl", i.e., left-associative infix operator.)
I noticed this too, when compiling the table of infix operators. This is
weird and should be cleared up. In fact, = and ~= and ≠ should all be
non-associative because there is no canonical orientation.
I think the "=" notation is going back to a time even before the 'infixl'
/ 'infixr' macros for the general mixfix form, and there were also some
special tweaks for output and breaks unlike regular infixes. 'infix' is
much younger than all that.
In the last 10 years, there have been some slight reforms towards more
regularity of notation for eq/not_equal in HOL. It might be worth trying
again to make it all just plain infix 50, although just from the
ancienticity of it it could cause some surprises in some dark corners.
This archive was generated by a fusion of
Pipermail (Mailman edition) and