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'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:

notation (output)
 blah_C ("moo")

then:
	typ "('a, 'p, blah_C) ptr_t"
prints:
	('a,'p,moo) 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?

That is a feature of all Isabelle versions until Isabelle2009-1. In Isabelle2009-2 the syntax becaume fully "authentic" after many years of reforming the system (see also the NEWS for Isabelle2009-2).

So the above should work properly, if this is really Isabelle2009-2.


	Makarius





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