[isabelle-dev] Notes on datatype_new list
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