# Re: [isabelle] Isabelle operator precedence

Dear Holger,
On 11/06/2012 04:59 AM, Holger Blasum wrote:

Now, for the cherry on the cake:
Where both parameters are equal (e.g. in the next line)
any[51] ">" any[51] => "\<^const>Orderings.ord_class_greater" (50)
Or the first one is larger than the second (rarely encountered,
but existing, e.g.)
logic[81] "respects" logic[80] => "\<^const>Equiv_Relations.RESPECTS" (80)
what does it mean for associativity?

When declaring infix syntax in thy files there are 3 possibilities:
- infix, for non-associative infix operators
- infixl, for left-associative infix operators
- infixr, for right-associative infix operators
and this corresponds to the following in the output of print_syntax
- both arguments have same number
- right argument has higher number
- left argument has higher number

`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.)
`
hope this helps,
chris

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