Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] datatype antiquotation

view this post on Zulip Email Gateway (Aug 18 2022 at 14:34):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Christian,

in your case I would suggest to modify the perl script ;-).

Hope this helps,
Florian
signature.asc

view this post on Zulip Email Gateway (Aug 18 2022 at 14:48):

From: Christian Sternagel <christian.sternagel@uibk.ac.at>
Hi there,

is there a way to rename type parameters in a datatype antiquotation? (I
didn't succeed in finding any documentation on this specific antiquotation.)

I have

datatype ('f,'v)term = Var 'v | Term 'f "('f,'v)term list"

but for document preparation I want (using the perl script
pretty_typvar, that Alexander provided me) to have nice Greek letters.
However, there is no Greek letter for "v", and something like
"(\<phi>,\<nu>)term" does look awkward. I would prefer
"(\<alpha>,\<beta>)term".

thnx in advance

cheers

chris

Last updated: Nov 21 2024 at 12:39 UTC