Re: [isabelle] Isabelle operator precedence



Hi Brian,

On 11-05, Brian Huffman wrote:
> If you want to have ALL the information about operator precedences,
> then have a look at the output of the "print_syntax" command. Under
> section "prods", the productions for the nonterminal "logic" are the
> main ones that you'll care about. For example:
> 
>  logic = any[65] "+" any[66] => "\<^const>Groups.plus_class.plus" (65)
> 
> This rule says that "+" is infix with precedence 65, and
> left-associative (evident from the fact that the left argument also
> requires precedence 65).

Very nice, at first glance that looks like exactly what I was 
looking for :-) 

If I get it right, this also shows that I was wrong with some of 
my conjectures:
	logic = "let" HOL.letbinds[0] "in" any[10] => "_Let" (10)
	logic = "if" logic[0] "then" any[0] "else" any[10] => "\<^const>HOL.If" (10)

=> let-in has the same precedence as if-then-else. (I'm not
completely sure what the "logic[0]" means here though.)

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?

Thanks,

-- 
Holger





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