doc-src/TutorialI/Misc/document/Option2.tex

Reintroduce set_interpreter for Collect and op :.
I removed them by accident when removing old code that dealt with the "set" type.
Incidentally, there is still some broken "set" code in Refute that should be fixed (see TODO in refute.ML).

%
\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%
\ {\isacharprime}a\ option\ {\isacharequal}\ None\ {\isacharbar}\ Some\ {\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: