[Agda] trouble with with

[Thorsten Altenkirch]

Thank you - this makes sense. Now it works - see attached.

Cheers,
Thorsten


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.

-------------- next part --------------
A non-text attachment was scrubbed...
Name: example.agda
Type: application/octet-stream
Size: 1107 bytes
Desc: not available
Url : https://lists.chalmers.se/mailman/private/agda/attachments/20080504/4c696b0e/example.obj
-------------- next part --------------



On 4 May 2008, at 18:43, Nils Anders Danielsson wrote:
> On Sun, May 4, 2008 at 4:14 PM, Thorsten Altenkirch  
> <txa at cs.nott.ac.uk> wrote:
>>
>>  plusView {succ m} {n} (fs i) with plusView {m} {n} i
>>  plusView {succ m} {n} .(fs (finl {m} {n} j)) | (inl {.m} {.n} j) = ?
>>  plusView {succ m} {n} .(fs (finr {m} {n} j)) | (inr {.m} {.n} j) = ?
>
> Agda complains because you have dotted the fs constructor. This code  
> works:
>
>  plusView {succ m} {n} (fs i) with plusView {m} {n} i
>  plusView {succ m} {n} (fs .(finl {m} {n} j)) | (inl {.m} {.n} j) = ?
>  plusView {succ m} {n} (fs .(finr {m} {n} j)) | (inr {.m} {.n} j) = ?
>
> -- 
> /NAD