Re: [isabelle] How do I make notation work only on the constant instead of on the type as well?
On 17/03/11 00:57, Makarius wrote:
On Wed, 16 Mar 2011, Rafal Kolanski wrote:
I meant Isabelle 2009-1. Do you know of any way of brute-forcing the
issue on this version?
Isabelle2009-1 does provide authentic syntax, but not for certain older
packages. So it depends what you mean by the following:
I have a structure whose constructor name is the same as its type.
Is this a HOL datatype? This is probably the most delicate situation.
I'm assuming it's something developed based on datatype code. It tries
to mimic a non-extensible recursive record.
For output of plain constructor terms, you can use 'abbreviation' with
its own notation (the const is authentic here). It does not work for
patterns, though. For example:
datatype blah_C = blah_C
where "blah_C_syntax == blah_C"
typ blah_C -- "blah_C"
term blah_C -- "moo"
term "case x of blah_C => y" -- "blah_C (!)"
This is perfect for the problem at hand. I don't really care what's
inside the type itself, only its record-like capabilities, so I will
never see a case statement like that, and certainly won't present it in
The authentic syntax in later versions sounds great too, it means my
"show constant names in a different font" notation hack (you have to
specify a list of them manually, but still) will work in future versions.
Thank you Makarius!
This archive was generated by a fusion of
Pipermail (Mailman edition) and