Hi Makarius,
>> (1) Its definition looks terrific:
>> datatype_new (set: 'a) list (map: map rel: list_all2) =
>> =: Nil (defaults tl: "[]") ("[]")
>> | Cons (hd: 'a) (tl: "'a list") (infixr "#" 65)
By all "means" terrific. :-)
>From Merriam-Webster dictionary, terrific can mean:
1: frightful
2: unusually fine
These items that the user traditionally takes the trouble to define "by hand"
are now provided
for free for any (co)datatype: the selectors and discriminators, the set
function, the relator.
These names that seem to clutter the specification are entirely optional -- if
not specified,
default names are produced.
You of course know all these, but I wanted to take this opportunity to
reiterate the advances
of the new (co)datatype.
Cheers,
Andrei
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
