[isabelle-dev] Notes on datatype_new list

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


 	Makarius