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 MHonArc.