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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
