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 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".


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.