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

abbreviation (output)
blah_C_syntax ("moo")
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 document.

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!

Rafal Kolanski.





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