[isabelle-dev] isabelle-dev Digest, Vol 84, Issue 31

Andrei Popescu uuomul at yahoo.com
Sat May 24 13:47:30 CEST 2014

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.  



More information about the isabelle-dev mailing list