Re: [isabelle] question on "notation"



On Sun, 11 Apr 2010, Christian Sternagel wrote:

today I stumbled over some (for me) unexpected behavior of the "notation" command.

I'm using the following notation:

 notation set ("\<^raw:\listset{>_\<^raw:}>")

where

 \newcommand\listset[1]{#1}

As soon as I have introduced the notation, however, all "set" types also use it. E.g., @{typ "('a * 'b) set"} is transformed into

 \isa{\listset{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b}}

The same behavior occurs when I'm defining notation for the constant "List.set" instead (and I do not see any connection between that constant and the type constructor "set").

The connection is the base name, which is "set" in both cases. Since the List.set constant uses non-authentic syntax for historical reasons, it is passed through the syntax layer via its base name only, causing confusion with the type constructor (all type constructors have non-authentic syntax).

This behaviour has been there in the syntax layer from the very beginning, and it is indeed unexpected. Only recently, I have finally managed to make syntax fully authentic: consts, types, classes as separate categories. So in the next official release the above should work as expected, at the cost of substantial incompatibility for most syntax translation functions by users out there.


My goal was to make the conversion from lists into sets 'implicit' in my resulting PDF. Any suggestions, how to achieve this?

You can try to exploit some further details in the syntax tree, using typed_print_translation for example: the const version should carry some type information, while the type version does not.


	Makarius






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