Re: [isabelle] term notation affects type parsing
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
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")
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".
This archive was generated by a fusion of
Pipermail (Mailman edition) and