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.