<html>
<head>
<meta content="text/html; charset=windows-1252"
http-equiv="Content-Type">
</head>
<body bgcolor="#FFFFFF" text="#000000">
Sorry, but what does "functions at type (Fin n -> Fin n) are
extensional" mean? I know what extensional equality is, and I am
assuming this is some related terminology, but I am not sure
precisely what.<br>
Thanks, <br>
Aaron<br>
<div class="moz-cite-prefix">On 02/18/2015 09:47 AM, João Paulo
Pizani Flor wrote:<br>
</div>
<blockquote
cite="mid:CAOwZJPTgH4gxF7YJUhm3WfLg8KT7fD42EY7PZ2tyV2m_-Oh-Ng@mail.gmail.com"
type="cite">
<div dir="ltr">
<div>Not yet (couldn't find it anywhere), but I will probably
need it for my Ph.D project, so maybe it will come in some
time...<br>
<br>
</div>
Cheers,<br>
<div>
<div>
<div class="gmail_extra"><br clear="all">
<div>
<div class="gmail_signature">
<div dir="ltr">
<div>
<div>João Pizani, M.Sc <<a
moz-do-not-send="true"
href="mailto:j.p.pizaniflor@uu.nl"
target="_blank">j.p.pizaniflor@uu.nl</a>><br>
</div>
Promovendus - Departement Informatica<br>
</div>
Faculteit Bètawetenschappen - Universiteit Utrecht<br>
</div>
</div>
</div>
<br>
<div class="gmail_quote">On Wed, Feb 18, 2015 at 3:25 PM,
Jacques Carette <span dir="ltr"><<a
moz-do-not-send="true"
href="mailto:carette@mcmaster.ca" target="_blank">carette@mcmaster.ca</a>></span>
wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0
.8ex;border-left:1px #ccc solid;padding-left:1ex">Does
anyone have a proof in Agda that functions at type
(Fin n -> Fin n) are extensional?<br>
Jacques<br>
_______________________________________________<br>
Agda mailing list<br>
<a moz-do-not-send="true"
href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a moz-do-not-send="true"
href="https://lists.chalmers.se/mailman/listinfo/agda"
target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote>
</div>
<br>
</div>
</div>
</div>
</div>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<br>
</body>
</html>