[Agda] Q: Matching Fin, Bug?

[Christoph Herrmann]

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
---

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

  The University of St Andrews is a charity registered in Scotland: No  
SC013532