[Agda] Pattern-matching operation order

[Ulf Norell]

On Tue, Feb 23, 2010 at 6:34 PM, Andreas Abel <andreas.abel at ifi.lmu.de>wrote:

> Thanks, Ulf, for the explanation.
>
> Is it fair to say that pattern matching works for all pattern inductive
> families, but not for those where indices are computed by (recursive)
> functions?
>

It still works. For instance, as long as the thing you match against have a
type where the index is a variable there are no problems.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20100223/6db1aaa7/attachment.html