<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 -&gt; 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 &lt;<a
                          moz-do-not-send="true"
                          href="mailto:j.p.pizaniflor@uu.nl"
                          target="_blank">j.p.pizaniflor@uu.nl</a>&gt;<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">&lt;<a
                    moz-do-not-send="true"
                    href="mailto:carette@mcmaster.ca" target="_blank">carette@mcmaster.ca</a>&gt;</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 -&gt; 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>