Email Gateway (Aug 18 2022 at 18:19): Email Gateway (Aug 18 2022 at 18:19):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Dear all,
when I declare syntax for a constant that coincides with the name of a type
constructor, Isabelle afterwards cannot parse the type name any more. Here's an
example:
typedecl mytype
consts foo :: "nat => nat"
notation foo ("mytype")
typ "mytype" (* fails with:
*** Inner syntax error at "mytype"
*** Failed to parse type
*** At command "typ"
*)
Why is this? I would have expected term and type syntax to be strictly separated
syntactic categories. Is there a mode on which I can restrict notation such that
it does not mess up type parsing?
Surprisingly, parsing works again if I add the following type_notation:
type_notation mytype ("mytype")
typ "mytype"
term "mytype"
Can I avoid the extra syntax notation for the type?
By the way, I used the RC1 of Isabelle2011-1.
Thanks for any help in advance,
Andreas
Email Gateway (Aug 18 2022 at 18:19):From: Makarius <makarius@sketis.net>
On Fri, 30 Sep 2011, Andreas Lochbihler wrote:
when I declare syntax for a constant that coincides with the name of a type
constructor, Isabelle afterwards cannot parse the type name any more. Here's
an example:typedecl mytype
consts foo :: "nat => nat"
notation foo ("mytype")
typ "mytype" (* fails with:*** Inner syntax error at "mytype"
*** Failed to parse type
*** At command "typ"
*)Why is this? I would have expected term and type syntax to be strictly
separated syntactic categories. Is there a mode on which I can restrict
notation such that it does not mess up type parsing?Surprisingly, parsing works again if I add the following type_notation:
type_notation mytype ("mytype")
typ "mytype"
term "mytype"Can I avoid the extra syntax notation for the type?
The syntactic categories of "logic" (for the term language) and "type"
(for the type language) are separate in the grammer, but they share the
same syntactic framework with a single lexical syntax. So "mytype" is
subtracted from the identifier category and cannot be used for plain type
names later on.
By the way, I used the RC1 of Isabelle2011-1.
Using the new Prover IDE (based on jEdit) in that version makes the
situation a bit more clear. The Term notation introduces a keyword
"mytype", and this is indicated by the colour scheme in the editor buffer
when writing typ "mytype".
Makarius
Last updated: Nov 21 2024 at 12:39 UTC