[isabelle-dev] Notes on datatype_new list

Dmitriy Traytel traytel at in.tum.de
Mon May 26 13:41:07 CEST 2014

Am 26.05.2014 12:53, schrieb Makarius:
> On Mon, 26 May 2014, Dmitriy Traytel wrote:
>>>  Just on the squiggles in isolation: if these are rare add-on 
>>> options one
>>>  could invent long / explicit keywords for them (or Parse.literal 
>>> items).
>> grep gives 371 occurences of "-:" in IsaFoR's development repository. 
>> So it's not a rare add-on, but an important performance optimization.
> If it is only an optimization it is conceptually still "rare". But of 
> course it is also possible to invent short keywords -- after some 
> empricial studies about the danger of clashing with common identifiers.
> The datatypes manual calls the above "dead" so that is an obvious 
> choice to try out.

Yes, we have considered this naming earlier. It was discarded, because 
it looks like one is giving the name "dead" to a set function. The same 
holds for any other identifier (not only the common ones). That was the 
reason to use something that is not an identifier.


More information about the isabelle-dev mailing list