[Agda] @-patterns

[Daniel Peebles]

There's an old ticket asking for this feature, but I don't think it's very
high on the priority list. I'm sure people would appreciate a patch, though
:)

http://code.google.com/p/agda/issues/detail?id=78&start=100

On Fri, Oct 5, 2012 at 1:38 PM, Serge D. Mechveliani <mechvel at botik.ru>wrote:

> It is better to write
>
>   f p@(prep2 x y xs x<=y ord-y-xs) =  prep2 0 x (y :: xs) z<=n p
>
> than
>
>   f (prep2 x y xs x<=y ord-y-xs) =  prep2 0 x (y :: xs) z<=n
>                                             (prep2 x y xs x<=y ord-y-xs)
>
> But  Agda-2.3.0.1  reports  "no @-patterns".
>
> Regards,
>
> ------
> Sergei
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20121005/00571cde/attachment.html