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