Yes, but the underlying reason for that is that complex numbers are isomorphic to pairs of real numbers, and binary product types are "degenerate" (I would rather say very basic) co-algebraic datatypes.
So my point (and I would guess Andrei's as well) is that this really has nothing to do with complex numbers, it is a general observation about types that are isomorphic to product types. In particular, any algebraic datatype with only one constructor can be rewritten into a corresponding codatatype, allowing you to use primcorec for it. Manuel On 13/05/14 13:39, Lawrence Paulson wrote: > 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 > <mailto: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
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
