Email Gateway (Aug 18 2022 at 15:03): Email Gateway (Aug 18 2022 at 15:03):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
Hi there,
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").
My goal was to make the conversion from lists into sets 'implicit' in my
resulting PDF. Any suggestions, how to achieve this?
cheers
chris
Email Gateway (Aug 18 2022 at 15:03):From: Makarius <makarius@sketis.net>
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
Last updated: Apr 30 2024 at 12:28 UTC