[isabelle] Antiquotations and Syntax Annotations



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!
-- 
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Coordenador do Curso de Ciência da Computação
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil




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