[Agda] Q: Matching Fin, Bug?

[Conor McBride]

Hi Christoph

On 1 Oct 2009, at 17:20, Christoph Herrmann 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

you could try adding

   f (suc (suc (suc ()))