[isabelle-dev] NEWS: avoid the Complex constructor, use the more natural

[Andrei Popescu]

I agree that functions to complex numbers (and products) are naturally definable using the selectors, and I very much appreciate what Johannes has been doing 
to systematically employ this view.  However, strictly speaking products are no more of a (degenerate) codatatype than sums are. 

Andrei



--------------------------------------------
On Tue, 5/13/14, Lawrence Paulson <lp15 at cam.ac.uk> wrote:

 Subject: Re: [isabelle-dev] NEWS: avoid the Complex constructor, use the more natural
 To: "Andrei Popescu" <uuomul at yahoo.com>
 Cc: "isabelle-dev at mailbroy.informatik.tu-muenchen.de" <isabelle-dev at mailbroy.informatik.tu-muenchen.de>
 Date: Tuesday, May 13, 2014, 2:39 PM
 
 it’s not just
 about syntactic sugar. It seems to me that the complex
 numbers are an elegant (if degenerative) example of a
 co-algebraic datatype. The co-recursive definitions look
 absolutely natural to me.
 
 Larry
 
 
 
 On 11 May 2014, at 12:55, Andrei Popescu <uuomul at yahoo.com>
 wrote:
 The fact that one can
 use primcorec to obtain the Re/Im view is simply a
 consequence of the syntactic sugar for the top 
 "sum of
 products" layer of (co)datatypes and the associated
 convenience for the (co)recursor.