[isabelle-dev] NEWS: avoid the Complex constructor, use the more natural
lp15 at cam.ac.uk
Tue May 13 13:39:50 CEST 2014
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.
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...
More information about the isabelle-dev