equal
deleted
inserted
replaced
1 % |
1 % |
2 \begin{isabellebody}% |
2 \begin{isabellebody}% |
3 \def\isabellecontext{Pairs}% |
3 \def\isabellecontext{Pairs}% |
4 % |
4 % |
5 \isamarkupsection{Pairs% |
5 \isamarkupsection{Pairs and Tuples% |
6 } |
6 } |
7 % |
7 % |
8 \begin{isamarkuptext}% |
8 \begin{isamarkuptext}% |
9 \label{sec:products} |
9 \label{sec:products} |
10 Pairs were already introduced in \S\ref{sec:pairs}, but only with a minimal |
10 Ordered pairs were already introduced in \S\ref{sec:pairs}, but only with a minimal |
11 repertoire of operations: pairing and the two projections \isa{fst} and |
11 repertoire of operations: pairing and the two projections \isa{fst} and |
12 \isa{snd}. In any non-trivial application of pairs you will find that this |
12 \isa{snd}. In any non-trivial application of pairs you will find that this |
13 quickly leads to unreadable formulae involving nests of projections. This |
13 quickly leads to unreadable formulae involving nests of projections. This |
14 section is concerned with introducing some syntactic sugar to overcome this |
14 section is concerned with introducing some syntactic sugar to overcome this |
15 problem: pattern matching with tuples.% |
15 problem: pattern matching with tuples.% |