Re: [isabelle] How do I make notation work only on the constant instead of on the type as well?
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.
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 archive was generated by a fusion of
Pipermail (Mailman edition) and