Re: [isabelle] Antiquotations and Syntax Annotations



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

Am 12/10/2012 13:50, schrieb Alfio Martini:
> 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!
> 





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