equal
deleted
inserted
replaced
1 (*<*) |
1 (*<*) |
2 theory pairs = Main:; |
2 theory pairs = Main:; |
3 (*>*) |
3 (*>*) |
4 text{*\label{sec:pairs}\indexbold{product type} |
4 text{*\label{sec:pairs}\indexbold{pair} |
5 \index{pair|see{product type}}\index{tuple|see{product type}} |
|
6 HOL also has pairs: \isa{($a@1$,$a@2$)} is of type $\tau@1$ |
5 HOL also has pairs: \isa{($a@1$,$a@2$)} is of type $\tau@1$ |
7 \indexboldpos{\isasymtimes}{$Isatype} $\tau@2$ provided each $a@i$ is of type |
6 \indexboldpos{\isasymtimes}{$Isatype} $\tau@2$ provided each $a@i$ is of type |
8 $\tau@i$. The components of a pair are extracted by \isaindexbold{fst} and |
7 $\tau@i$. The components of a pair are extracted by \isaindexbold{fst} and |
9 \isaindexbold{snd}: |
8 \isaindexbold{snd}: |
10 \isa{fst($x$,$y$) = $x$} and \isa{snd($x$,$y$) = $y$}. Tuples |
9 \isa{fst($x$,$y$) = $x$} and \isa{snd($x$,$y$) = $y$}. Tuples |