[isabelle-dev] Notes on datatype_new list

[Jasmin Blanchette]

Am 26.05.2014 um 12:25 schrieb Makarius <makarius at sketis.net>:

> 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).

Right, let's get the squiggles out of the way.

For "=:", let's make this the default, so that no keyword is needed. Andreas L. argued against, but it's easy to override by providing a name, and the two main datatypes in Isabelle/HOL, "list" and "option", both use it.

For "-:", this is indeed a rare add-on option (but an important one to some people).

Also, the single worst aspect of the current "list" definition -- the "=: " syntax -- could be changed so that this is the default. (It used to be.)

Am 26.05.2014 um 13:41 schrieb Dmitriy Traytel <traytel at in.tum.de>:

> 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.

Right. On the other hand, it's hard to imagine anybody giving the name "dead" to the set of values associated with a so called *live* type variable, so perhaps it's not too bad a choice.

Also, I agree with Makarius that it is a rare optimization. IsaFoR is a very atypical application (and in fact most of the 371 occurrences could be avoided without changing anything, because "deadness" is inherited when composing BNFs).

Jasmin