[isabelle-dev] Notes on datatype_new list

[Dmitriy Traytel]

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.

Dmitriy