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
