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)
.