[Agda] Q: Matching Fin, Bug?

[Liang-Ting Chen]

Hi,

On Fri, Oct 2, 2009 at 12:20 AM, Christoph Herrmann
<ch at cs.st-andrews.ac.uk>wrote:

> Hi,
>
> maybe I'm doing something wrong or there is a bug, but in the following
> program
> Agda complains about incomplete pattern matching:
> ---
> module T where
>
> open import Data.Fin
>
> f : Fin 3 → Fin 3
> f zero = suc zero
> f (suc zero) = suc (suc zero)
> f (suc (suc zero)) = zero
>
Add the following line,

f (suc (suc (suc ())))

> ---
>
> Best Wishes
> --
>  Dr. Christoph Herrmann
>  University of St Andrews, Scotland/UK
>  phone: office: +44 1334 461629, home: +44 1334 478648
>  email: ch at cs.st-andrews.ac.uk,  c.herrmann at virgin.net
>  URL:   http://www.cs.st-andrews.ac.uk/~ch<http://www.cs.st-andrews.ac.uk/%7Ech>
>
>  The University of St Andrews is a charity registered in Scotland: No
> SC013532
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>


-- 
sincerely,
Liang-Ting
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20091002/5f6a54a5/attachment.html