[Agda] coverage in Agda-2.1.3

[Thorsten Altenkirch]

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.