Email Gateway (Aug 19 2022 at 08:58): Email Gateway (Aug 19 2022 at 08:58):From: Alfio Martini <alfio.martini@acm.org>
Dear Isabelle Users,
When defining datatypes with syntax annotations, the usual commands @{term
"..."}, @{const "..."} present the
corresponding expressions with the alternative syntax, even if specified
otherwise.
For instance, assuming the declaration below
datatype 'a List = Nil ("[]")
| Cons 'a "'a List" (infixr "#" 65)
we have the following:
@{term "Nil"} produces "[]" (wanted "Nil")
@{term "Cons"} produces "op #" (wanted "Cons") [tried @{const "Cons"}, but
it does not work either]
@{term "Cons h t"} produces "(h::'a) # (t::'a List)" (wanted "Cons h t").
When I want types I use term_type or show_types.
Anyway, judging from the way the tutorial (section 4.1.1, definition and
discussion of "xor") I assume this kind of
control is possible with the available resources.
I could use @{text "..."}, but this would be plain and simple humiliation.
Thanks for any help on that!
Email Gateway (Aug 19 2022 at 08:58):From: Tobias Nipkow <nipkow@in.tum.de>
You can write @{term [source] "..."} and it checks and prints your term as you
gave it - unfortunately including the quotation marks. You can work around that
by setting the quotation marks temporarily to empty:
\newcommand{\noquotes}[1]{{\renewcommand{\isachardoublequote}{}\renewcommand{\isachardoublequoteopen}{}\renewcommand{\isachardoublequoteclose}{}#1}}
If you never want to see them, then you can of course do the above
\renewcommands globally.
Tobias
Email Gateway (Aug 19 2022 at 08:58):From: Alfio Martini <alfio.martini@acm.org>
Good to know about that! Thank you again!
Last updated: Apr 23 2024 at 20:15 UTC