[isabelle-dev] isabelle-dev Digest, Vol 84, Issue 31
uuomul at yahoo.com
Sat May 24 13:47:30 CEST 2014
>> (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:
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.
More information about the isabelle-dev