[Agda] coverage in Agda-2.1.3

[Ana Bove]

> In any case, how would I fill in this case? I tried
>
>   fpair : forall {m n} -> Fin m -> Fin n -> Fin (m × n)
>   fpair {zero}   {n} i      ()
>   fpair {succ m} {n} fz     i = finl {n} {m × n} i
>   fpair {succ m} {n} (fs j) i = finr {n} {m × n} (fpair j i)
>
> but Agda says (in the ghci buffer !?)
>
> Fin n should be empty, but it isn't (as far as I can see)
> when checking that the clause fpair {zero} {n} i () has type ...

bit you have put i : Fin m and () in the case of Fin n while you should 
have done the other way around!

-- 
-- Ana

************************************************************************
                                ANA  BOVE
 bove(at)cs.chalmers.se  Department of Computer Science and Engineering
 http://www.cs.chalmers.se/~bove      Chalmers University of Technology
 Phone (work) :(46)(31) 772 10 20          and University of Gothenburg
 Fax (work)   :(46)(31) 772 36 63        S-412 96 Gothenburg  -  SWEDEN
************************************************************************