|
10561
|
1 |
%
|
|
|
2 |
\begin{isabellebody}%
|
|
|
3 |
\def\isabellecontext{Option{\isadigit{2}}}%
|
|
11866
|
4 |
\isamarkupfalse%
|
|
|
5 |
\isamarkupfalse%
|
|
|
6 |
\isamarkupfalse%
|
|
10561
|
7 |
%
|
|
|
8 |
\begin{isamarkuptext}%
|
|
11428
|
9 |
\indexbold{*option (type)}\indexbold{*None (constant)}%
|
|
|
10 |
\indexbold{*Some (constant)}
|
|
10561
|
11 |
Our final datatype is very simple but still eminently useful:%
|
|
|
12 |
\end{isamarkuptext}%
|
|
11866
|
13 |
\isamarkuptrue%
|
|
|
14 |
\isacommand{datatype}\ {\isacharprime}a\ option\ {\isacharequal}\ None\ {\isacharbar}\ Some\ {\isacharprime}a\isamarkupfalse%
|
|
|
15 |
%
|
|
10561
|
16 |
\begin{isamarkuptext}%
|
|
|
17 |
\noindent
|
|
11310
|
18 |
Frequently one needs to add a distinguished element to some existing type.
|
|
10561
|
19 |
For example, type \isa{t\ option} can model the result of a computation that
|
|
|
20 |
may either terminate with an error (represented by \isa{None}) or return
|
|
|
21 |
some value \isa{v} (represented by \isa{Some\ v}).
|
|
|
22 |
Similarly, \isa{nat} extended with $\infty$ can be modeled by type
|
|
|
23 |
\isa{nat\ option}. In both cases one could define a new datatype with
|
|
|
24 |
customized constructors like \isa{Error} and \isa{Infinity},
|
|
|
25 |
but it is often simpler to use \isa{option}. For an application see
|
|
|
26 |
\S\ref{sec:Trie}.%
|
|
|
27 |
\end{isamarkuptext}%
|
|
11866
|
28 |
\isamarkuptrue%
|
|
|
29 |
\isamarkupfalse%
|
|
10561
|
30 |
\end{isabellebody}%
|
|
|
31 |
%%% Local Variables:
|
|
|
32 |
%%% mode: latex
|
|
|
33 |
%%% TeX-master: "root"
|
|
|
34 |
%%% End:
|