[Agda] trouble with with

[Nils Anders Danielsson]

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