[isabelle-dev] Notes on datatype_new list

[Dmitriy Traytel]

Am 26.05.2014 12:25, schrieb Makarius:
> On Sun, 25 May 2014, Jasmin Christian Blanchette wrote:
>
>> The "=" as the name for Nil's discriminator deserves an explanation. 
>> [...] So I introduced this weird "=" syntax, which suggests that 
>> equality is used for discriminating. I am open to other suggestions.
>>
>> The other funky syntax we have is "-:". E.g.
>>
>>    datatype_new (-: 'a) list = ...
>>
>> This says: Don't generate a set function for 'a -- and don't allow 
>> nesting through lists.
>
> 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.

Dmitriy