[Agda] @-patterns

Serge D. Mechveliani mechvel at botik.ru
Fri Oct 5 20:02:02 CEST 2012

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.



More information about the Agda mailing list