<html>
<head>
<meta content="text/html; charset=ISO-8859-1"
http-equiv="Content-Type">
</head>
<body bgcolor="#FFFFFF" text="#000000">
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.<br>
<br>
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.<br>
<br>
Manuel<br>
<br>
<div class="moz-cite-prefix">On 13/05/14 13:39, Lawrence Paulson
wrote:<br>
</div>
<blockquote
cite="mid:AD71A740-CB16-45AF-8970-D30EE62B60FA@cam.ac.uk"
type="cite">
<meta http-equiv="Content-Type" content="text/html;
charset=ISO-8859-1">
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.<br>
<div apple-content-edited="true">
<span class="Apple-style-span" style="border-collapse: separate;
color: rgb(0, 0, 0); font-family: Helvetica; font-size: 11px;
font-style: normal; font-variant: normal; font-weight: normal;
letter-spacing: normal; line-height: normal; orphans: 2;
text-align: auto; text-indent: 0px; text-transform: none;
white-space: normal; widows: 2; word-spacing: 0px;
-webkit-border-horizontal-spacing: 0px;
-webkit-border-vertical-spacing: 0px;
-webkit-text-decorations-in-effect: none;
-webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0;
">Larry</span>
</div>
<br>
<div>
<div>On 11 May 2014, at 12:55, Andrei Popescu <<a
moz-do-not-send="true" href="mailto:uuomul@yahoo.com">uuomul@yahoo.com</a>>
wrote:</div>
<br class="Apple-interchange-newline">
<blockquote type="cite"><span style="font-family: HelveticaNeue,
'Helvetica Neue', Helvetica, Arial, 'Lucida Grande',
sans-serif; font-size: 16px; font-style: normal;
font-variant: normal; font-weight: normal; letter-spacing:
normal; line-height: normal; orphans: auto; text-align:
start; text-indent: 0px; text-transform: none; white-space:
normal; widows: auto; word-spacing: 0px;
-webkit-text-stroke-width: 0px; background-color: rgb(255,
255, 255); float: none; display: inline !important;">The
fact that one can use primcorec to obtain the Re/Im view is
simply a consequence of the syntactic sugar for the top<span
class="Apple-converted-space"> </span></span><br class=""
style="font-family: HelveticaNeue, 'Helvetica Neue',
Helvetica, Arial, 'Lucida Grande', sans-serif; font-size:
16px; font-style: normal; font-variant: normal; font-weight:
normal; letter-spacing: normal; line-height: normal;
orphans: auto; text-align: start; text-indent: 0px;
text-transform: none; white-space: normal; widows: auto;
word-spacing: 0px; -webkit-text-stroke-width: 0px;
background-color: rgb(255, 255, 255);">
<span style="font-family: HelveticaNeue, 'Helvetica Neue',
Helvetica, Arial, 'Lucida Grande', sans-serif; font-size:
16px; font-style: normal; font-variant: normal; font-weight:
normal; letter-spacing: normal; line-height: normal;
orphans: auto; text-align: start; text-indent: 0px;
text-transform: none; white-space: normal; widows: auto;
word-spacing: 0px; -webkit-text-stroke-width: 0px;
background-color: rgb(255, 255, 255); float: none; display:
inline !important;">"sum of products" layer of (co)datatypes
and the associated convenience for the (co)recursor. <span
class="Apple-converted-space"> </span></span><br class=""
style="font-family: HelveticaNeue, 'Helvetica Neue',
Helvetica, Arial, 'Lucida Grande', sans-serif; font-size:
16px; font-style: normal; font-variant: normal; font-weight:
normal; letter-spacing: normal; line-height: normal;
orphans: auto; text-align: start; text-indent: 0px;
text-transform: none; white-space: normal; widows: auto;
word-spacing: 0px; -webkit-text-stroke-width: 0px;
background-color: rgb(255, 255, 255);">
</blockquote>
</div>
<br>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
isabelle-dev mailing list
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<a class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a>
</pre>
</blockquote>
<br>
</body>
</html>