Re: [isabelle] Isabelle operator precedence



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

- Brian

On Mon, Nov 5, 2012 at 3:23 PM, Holger Blasum <hbl at sysgo.com> wrote:
> Dear all,
>
> while it is mostly "intuitive" I would like to have a clearer view of
> operator precedence in Isabelle. Attached is what I quickly reverse-
> engineered on a train ride on the long weekend. Is it correct? Is there
> already any explicit information on this (beyond using
> Isabelle -> Settings -> Display -> Show Brackets in PG)?
>
> Thanks,
>
> --
> Holger





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