Am 26.05.2014 um 12:25 schrieb Makarius <makar...@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 <tray...@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

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to