Email Gateway (Aug 19 2022 at 17:00): Email Gateway (Aug 19 2022 at 17:00):From: "W. Douglas Maurer" <maurer@gwu.edu>
On p. 11 of the document "Whats In Main" there is a very useful table
giving, for every infix operator in Main, its precedence as an
integer between 0 and 100, and its associativity (either left or
right).
I would like to ask: Is there anything like this for the Isar type operators?
All I have been able to find in the reference manuals and tutorials
is relative precedence. So for example (p. 3 of prog-prove): "Note
that 'a => 'b list means 'a => ('b list), not ('a => 'b) list :
postfix type constructors have precedence over => ."
This answers some of the obvious questions about type operator
precedence, but not all of them. There should be a table from which I
can deduce the answers to questions like: Why the parentheses in (int
Email Gateway (Aug 19 2022 at 17:00):From: Makarius <makarius@sketis.net>
On Sun, 25 Jan 2015, W. Douglas Maurer wrote:
Is there anything like this for the Isar type operators?
I was first confused by that. The type operators are part of the logical
language of Pure or HOL, not the theory and proof language of Isar.
All I have been able to find in the reference manuals and tutorials is
relative precedence. So for example (p. 3 of prog-prove): "Note that 'a
=> 'b list means 'a => ('b list), not ('a => 'b) list : postfix type
constructors have precedence over => ."
The function space is part of Pure, and the "isar-ref" manual has section
7.4.3 The Pure grammar. You can also use the print_syntax command, but
its output is a bit large (in theory Pure it is still manageable).
This answers some of the obvious questions about type operator precedence,
but not all of them. There should be a table from which I can deduce the
answers to questions like: Why the parentheses in (int * int) set ? Do
postfix type constructors also have precedence over * as well as over => ?
Such a table, in addition to covering postfix type constructors (list, set,
rel, etc.) and * (for product type), should cover / (for quotient type), =>
(for function types), and all the other type operators.
Like in the term language, application for types binds most tightly, so
you need parentheses for arguments with separate structure. The Pure
grammar reveals that as well.
Makarius
Last updated: Apr 20 2024 at 04:19 UTC