[Agda] @-patterns

[Daniel Peebles]

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 for more complicated things, Agda's going to forget that p = prep2 ...,
 so you might need to jump through some hoops to get it to notice that
again.

Hope this helps,
Dan

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/7ececd83/attachment.html