%
\begin{isabellebody}%
\def\isabellecontext{Option{\isadigit{2}}}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\begin{isamarkuptext}%
\indexbold{*option (type)}\indexbold{*None (constant)}%
\indexbold{*Some (constant)}
Our final datatype is very simple but still eminently useful:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{datatype}\isamarkupfalse%
\ {\isaliteral{27}{\isacharprime}}a\ option\ {\isaliteral{3D}{\isacharequal}}\ None\ {\isaliteral{7C}{\isacharbar}}\ Some\ {\isaliteral{27}{\isacharprime}}a%
\begin{isamarkuptext}%
\noindent
Frequently one needs to add a distinguished element to some existing type.
For example, type \isa{t\ option} can model the result of a computation that
may either terminate with an error (represented by \isa{None}) or return
some value \isa{v} (represented by \isa{Some\ v}).
Similarly, \isa{nat} extended with $\infty$ can be modeled by type
\isa{nat\ option}. In both cases one could define a new datatype with
customized constructors like \isa{Error} and \isa{Infinity},
but it is often simpler to use \isa{option}. For an application see
\S\ref{sec:Trie}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: