*To*: Brian Huffman <huffman at in.tum.de>*Subject*: Re: [isabelle] Isabelle operator precedence*From*: Holger Blasum <hbl at sysgo.com>*Date*: Mon, 5 Nov 2012 20:59:10 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <CAAMXsiaSBptcj3swFrbBFAOZdZ=iSZhJRQEwbC5wBLeRy_v7QQ@mail.gmail.com>*References*: <20121105142302.GA10786@laptop-hbl.localdomain> <CAAMXsiaSBptcj3swFrbBFAOZdZ=iSZhJRQEwbC5wBLeRy_v7QQ@mail.gmail.com>*User-agent*: Mutt/1.5.21 (2010-09-15)

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

**Follow-Ups**:**Re: [isabelle] Isabelle operator precedence***From:*Christian Sternagel

**Re: [isabelle] Isabelle operator precedence***From:*Holger Gast

**References**:**[isabelle] Isabelle operator precedence***From:*Holger Blasum

**Re: [isabelle] Isabelle operator precedence***From:*Brian Huffman

- Previous by Date: Re: [isabelle] Isabelle operator precedence
- Next by Date: [isabelle] looking for some measure.union_inter theorem
- Previous by Thread: Re: [isabelle] Isabelle operator precedence
- Next by Thread: Re: [isabelle] Isabelle operator precedence
- Cl-isabelle-users November 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list