[Agda] @-patterns

[Serge D. Mechveliani]

On Fri, Oct 05, 2012 at 01:47:29PM -0400, Daniel Peebles wrote:
> An alternative is to write something like
> 
> f p with p
> ...  | prep2 x y xs x<=y ord-y-xs = prep2 0 x (y :: xs) z<=n p
> 
> [..]

But in my example  f (prep2 x y xs x<=y ord-y-xs)  is the last pattern  
in a complete pattern sequence.
I did try `with', but then Agda asked for further patters  `... | ...',
it does not notice that the patterns have been exhausted earlier.

I do not insist on its high priority, just reported a feature, for future.

Regards,

------
Sergei