(*<*) theory Option2 imports Main begin
hide_const None Some
hide_type option (*>*)
text‹\indexbold{*option (type)}\indexbold{*None (constant)}%
indexbold{*Some (constant)}
final datatype is very simple but still eminently useful: ›
datatype 'a option = None | Some 'a
text‹\noindent
one needs to add a distinguished element to some existing type.
example, type ‹t option› can model the result of a computation that
either terminate with an error (represented by const‹None›) or return
value term‹v› (represented by term‹Some v›).
, typ‹nat› extended with $\infty$ can be modeled by type typ‹nat option›. In both cases one could define a new datatype with
constructors like term‹Error› and term‹Infinity›,
it is often simpler to use ‹option›. For an application see
S\ref{sec:Trie}. › (*<*) (* definitioninfplus::"natoption\<Rightarrow>natoption\<Rightarrow>natoption"where "infplusxy\<equiv>casexofNone\<Rightarrow>None |Somem\<Rightarrow>(caseyofNone\<Rightarrow>None|Somen\<Rightarrow>Some(m+n))"
*) end (*>*)
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.10 Sekunden
(vorverarbeitet am 2026-06-30)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
