[Agda] coverage in Agda-2.1.3

[Ana Bove]

However, your original comments is still interesting to understand. I 
would also agree with you that we do have exhaustive patterns. Actually, 
this is a correct partial program in 2.1.3

fpair : forall {m n} -> Fin m -> Fin n -> Fin (m * n)
fpair fzero     i = ?
fpair (fsucc j) i = ?

I would have expect then that dotting the m will do it

fpair : forall {m n} -> Fin m -> Fin n -> Fin (m * n)
fpair {.(succ m)} {n} fzero     i = ?
fpair {.(succ m)} {n} (fsucc j) i = ?

but it does not....

Best

Thorsten Altenkirch wrote:
> Thank you, Ana. I didn't understand the () properly - the following 
> seems to work:
>
>   fpair : forall {m n} -> Fin m -> Fin n -> Fin (m × n)
>   fpair {zero}   {n} ()     _
>   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)
>
> Cheers,
> Thorsten
>
> On 7 May 2008, at 11:08, Ana Bove wrote:
>
>>
>>> 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
>> ************************************************************************
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>
>
> This message has been checked for viruses but the contents of an 
> attachment
> may still contain software viruses, which could damage your computer 
> system:
> you are advised to perform your own checks. Email communications with the
> University of Nottingham may be monitored as permitted by UK legislation.
>

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