[isabelle-dev] Notes on datatype_new list
traytel at in.tum.de
Mon May 26 12:34:22 CEST 2014
Am 26.05.2014 12:25, schrieb 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
grep gives 371 occurences of "-:" in IsaFoR's development repository. So
it's not a rare add-on, but an important performance optimization.
More information about the isabelle-dev