Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] arities syntax in Isar-style theory files

Email Gateway (Aug 18 2022 at 09:38):

From: Jeremy Dawson <Jeremy.Dawson@rsise.anu.edu.au>
The reference manual gives the following example

arities
foo :: ({logic}) logic
foo :: ({}) term

(which is syntactically accepted in an old-style theory though
it produces an error)

But in an Isar-style theory it is rejected with the following
message

*** Outer syntax error (line 33 of
"/home/users/jeremy/isabelle/cat/kozen.thy"): sort expected,
*** but command "{" (line 33 of
"/home/users/jeremy/isabelle/cat/kozen.thy") was found

The Isar ref manual documentation leaves me confused.

Does anyone know what is the Isar equivalent for the example above?

Jeremy

Email Gateway (Aug 18 2022 at 09:39):

From: Brian Huffman <brianh@csee.ogi.edu>
Try using quotes around the braces, like this:

arities
foo :: ("{logic}") logic
foo :: ("{}") term

The parser for sorts (defined in Pure/Isar/outer_syntax.ML) can accept an
alphanumeric name, or a quoted string, but not anything starting with a
curly-brace character. I think the confusion in the reference manual might
arise because quote marks are omitted when Isabelle syntax is typeset.

Hope this helps.

• Brian Huffman

Last updated: May 03 2024 at 04:19 UTC