Tuple patterns

A tuple pattern consists of a tuple expression (i.e. a pair, triple, …) used as a pattern. Each component of the tuple can itself be any pattern. The simplest kind of tuple pattern would be a pair with variables, like

f : N * N -> Q
f(x,y) = ...

This is extremely common when defining functions that take multiple inputs. Functions that take more than two inputs can also be defined similarly:

f : N * Z * Z -> Z
f(a,b,c) = ...

(See the page on pair types for more details on how n-tuples work.)

The components of a pair pattern can themselves be any pattern, however, not just variables. For example,

f : N * N -> N
f(2n+1, 3) = 17
f(x, y) = x + y

The above example defines f to yield 17 when applied to any tuple consisting of an odd number paired with 3 (using an arithmetic pattern and a literal pattern), and x + y when applied to any other pair (x,y).