[Agda] trouble with "with"

[Thorsten Altenkirch]

Hi everybody,

I hope you all had a nice christmas. I am playing around with Agda  
while my son is liberating the universe on the playstation.

However, I got badly stuck on a with pattern. Agda tells me that it  
"Cannot split on the constructor vapp". What does this actually mean?

I attach the relevant pieces of my code. The idea is to implement the  
fact that neutral normal forms (x t1 .. tn) can either be viewed from  
the left or from the right.
I take the left view as primitive and derive the spine view as a view.

This is basically the idea that lists can be viewed as snoc lists but  
with types.

Any advice would be appreciated.


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: problem.agda
Type: application/octet-stream
Size: 1469 bytes
Desc: not available
Url : https://lists.chalmers.se/mailman/private/agda/attachments/20081229/6d40ac6c/problem.obj
-------------- next part --------------



Cheers,
Thorsten