[isabelle] How do I make notation work only on the constant instead of on the type as well?
- To: isabelle-users at cl.cam.ac.uk
- Subject: [isabelle] How do I make notation work only on the constant instead of on the type as well?
- From: Rafal Kolanski <rafalk at cse.unsw.edu.au>
- Date: Wed, 16 Mar 2011 22:50:26 +1100
- User-agent: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:126.96.36.199) Gecko/20101208 Thunderbird/3.1.7
Dear Isabelle Users,
I'm on Isabelle 2009-2, and I'm stuck with the following problem. I have
a structure whose constructor name is the same as its type. For
presentation in LaTeX I'm using a notation hack which makes constants a
different font than normal isabelle text.
Here's the problem. I define notation as:
typ "('a, 'p, blah_C) ptr_t"
and: term "blah_C x y z" prints: "moo x y z" :: moo
Why does output notation pick up on the type, when I'm not using a type
translation? How do I specify I want the constant blah_C as the target
of my notation and not the type?
I realise that the same constructor and type name is not ideal, but the
output does not come from a tool written by me.
This archive was generated by a fusion of
Pipermail (Mailman edition) and