Email Gateway (Aug 18 2022 at 20:29): Email Gateway (Aug 18 2022 at 20:29):From: chunhan wu <wuchunhan@gmail.com>
Hi,
I tried the following:
type_synonym my_int = int
text {* @{typ my_int} *}
datatype foo = A | B my_int
text {* @{datatype foo} *}
The "text" works and prints out "my_int",
but the "datatype" prints out "int"
which should be "my_int".
Is there an attribute for datatype antiquotation
to solve this problem?
Regards,
Chunhan
Email Gateway (Aug 18 2022 at 20:30):From: Tobias Nipkow <nipkow@in.tum.de>
Type synonyms are expanded during parsing. They beautify the input but cannot
occur in the output.
Tobias
Email Gateway (Aug 18 2022 at 20:30):From: Ramana Kumar <rk436@cam.ac.uk>
On Tue, Jul 17, 2012 at 8:22 AM, Tobias Nipkow <nipkow@in.tum.de> wrote:
Type synonyms are expanded during parsing. They beautify the input but cannot
occur in the output.
In HOL4, the printer attempts to use user-defined type synonyms when
possible, helping increase consistency between input and output.
Sometimes, of course, if you have many synonyms for the same type, you
get the wrong one printed.
Was it a principled decision not to print synonyms in Isabelle?
Tobias
Am 16/07/2012 12:25, schrieb chunhan wu:
Hi,
I tried the following:
type_synonym my_int = int
text {* @{typ my_int} *}
datatype foo = A | B my_int
text {* @{datatype foo} *}
The "text" works and prints out "my_int",
but the "datatype" prints out "int"
which should be "my_int".Is there an attribute for datatype antiquotation
to solve this problem?Regards,
Chunhan
Email Gateway (Aug 18 2022 at 20:30):From: Tobias Nipkow <nipkow@in.tum.de>
Am 17/07/2012 09:29, schrieb Ramana Kumar:
On Tue, Jul 17, 2012 at 8:22 AM, Tobias Nipkow <nipkow@in.tum.de> wrote:
Type synonyms are expanded during parsing. They beautify the input but cannot
occur in the output.In HOL4, the printer attempts to use user-defined type synonyms when
possible, helping increase consistency between input and output.
Sometimes, of course, if you have many synonyms for the same type, you
get the wrong one printed.
Was it a principled decision not to print synonyms in Isabelle?
Yes.
Tobias
Tobias
Am 16/07/2012 12:25, schrieb chunhan wu:
Hi,
I tried the following:
type_synonym my_int = int
text {* @{typ my_int} *}
datatype foo = A | B my_int
text {* @{datatype foo} *}
The "text" works and prints out "my_int",
but the "datatype" prints out "int"
which should be "my_int".Is there an attribute for datatype antiquotation
to solve this problem?Regards,
Chunhan
Email Gateway (Aug 18 2022 at 20:31):From: Makarius <makarius@sketis.net>
The question of reverting type synonyms pops up every couple of years, and
I have reconsidered it myself many times already. There have been
counter-indications both from users getting confused about arbitrary
type-subexpressions being subject to contraction, and technical problems
in the interaction with other syntax mechanisms (such as translations that
may depend on type information).
So Isabelle does not support that, and probably never will support it.
Nonetheless, some libraries try to simulate it via 'translations' for the
ASTs stemming from types, but this causes other surprises (as I've just
seen again in the output of 'print_theory' yesterday).
Makarius
Last updated: Apr 26 2024 at 04:17 UTC