Re: n+k patterns

[marc]

>From my point of view (n+k)-patterns have a
very special meaning. This natural numbers
should be considered as a type like this:

data Nat = Zero | Succ Nat

Therefore a (n+k)-pattern is an abbreviation for
Succ(Succ(...Zero...)). It's obvious that
"+" in "(n+k)" doesn't mean a somewhere
else defined (or locally rebound) function.

If we keep this in mind there shouldn't
be any problem.


(Tell me if I'm wrong.)

Greetings,

Marc Rehmsmeier.