Hi, <br><br><div class="gmail_quote">On Fri, Oct 2, 2009 at 12:20 AM, Christoph Herrmann <span dir="ltr">&lt;<a href="mailto:ch@cs.st-andrews.ac.uk">ch@cs.st-andrews.ac.uk</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">

Hi,<br>
<br>
maybe I&#39;m doing something wrong or there is a bug, but in the following program<br>
Agda complains about incomplete pattern matching:<br>
---<br>
module T where<br>
<br>
open import Data.Fin<br>
<br>
f : Fin 3 → Fin 3<br>
f zero = suc zero<br>
f (suc zero) = suc (suc zero)<br>
f (suc (suc zero)) = zero<br></blockquote><div>Add the following line,<br><br>f (suc (suc (suc ())))<br></div><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">


---<br>
<br>
Best Wishes<br>
-- <br>
 Dr. Christoph Herrmann<br>
 University of St Andrews, Scotland/UK<br>
 phone: office: +44 1334 461629, home: +44 1334 478648<br>
 email: <a href="mailto:ch@cs.st-andrews.ac.uk" target="_blank">ch@cs.st-andrews.ac.uk</a>,  <a href="mailto:c.herrmann@virgin.net" target="_blank">c.herrmann@virgin.net</a><br>
 URL:   <a href="http://www.cs.st-andrews.ac.uk/%7Ech" target="_blank">http://www.cs.st-andrews.ac.uk/~ch</a><br>
<br>
 The University of St Andrews is a charity registered in Scotland: No SC013532<br>
<br>
<br>
<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br>
</blockquote></div><br><br clear="all"><br>-- <br>sincerely, <br>Liang-Ting<br>