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 <l...@cam.ac.uk> wrote: Subject: Re: [isabelle-dev] NEWS: avoid the Complex constructor, use the more natural To: "Andrei Popescu" <uuo...@yahoo.com> Cc: "isabelle-dev@mailbroy.informatik.tu-muenchen.de" <isabelle-dev@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 <uuo...@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. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
