[isabelle-dev] Notes on datatype_new list

Makarius makarius at sketis.net
Mon May 26 12:25:33 CEST 2014

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


More information about the isabelle-dev mailing list