[isabelle-dev] NEWS: avoid the Complex constructor, use the more natural
uuomul at yahoo.com
Tue May 13 15:42:35 CEST 2014
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.
On Tue, 5/13/14, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
Subject: Re: [isabelle-dev] NEWS: avoid the Complex constructor, use the more natural
To: "Andrei Popescu" <uuomul at yahoo.com>
Cc: "isabelle-dev at mailbroy.informatik.tu-muenchen.de" <isabelle-dev at 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.
On 11 May 2014, at 12:55, Andrei Popescu <uuomul at yahoo.com>
The fact that one can
use primcorec to obtain the Re/Im view is simply a
consequence of the syntactic sugar for the top
products" layer of (co)datatypes and the associated
convenience for the (co)recursor.
More information about the isabelle-dev