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

[Lawrence Paulson]

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.  

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20140513/67ff6a13/attachment-0002.html>