Re: [isabelle] Isabelle operator precedence

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.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.