[Agda] Pattern-matching operation order

[Dan Licata]

On Feb23, Ulf Norell wrote:
> 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.

Also, being a pattern inductive family isn't a sufficient condition:
there are times when you can't pattern-match on an inhabitant of a
pattern inductive family. E.g.

  f : {A : Set} {n : Nat} {f : Nat -> Nat} -> Vec A (f n) -> Unit
  f v = {!v!}

you can't match on 'v'. 

-Dan