Quelle Option2.thy

Sprache: Isabelle

(*<*)
theory Option2 imports Main begin
hide_const None Some
hide_type option
(*>*)

text‹\indexbold{*option (type)}\indexbold{*None (constant)}%
\indexbold{*Some (constant)}
Our final datatype is very simple but still eminently useful:
›

datatype 'a option = None | Some 'a

text‹\noindent
Frequently one needs to add a distinguished element to some existing type.
For example, type ‹t option› c
may either terminate with an error (represented by 🍋‹None›) or return
some value 🍋‹v› (represented by 🍋‹Some v›).
Similarly, 🍋‹nat› extended with $\infty$ can be modeled by type
🍋‹nat option›. In both cases one could define a new datatype with
customized constructors like 🍋‹Error› and 🍋‹Infinity›,
but it is often simpler to use ‹option›. For an application see
\S\ref{sec:Trie}.
›
(*<*)
(*
definition infplus :: "nat option ==> nat option ==> nat option" where
"infplus x y ≡ case x of None ==> None
| Some m ==> (case y of None ==> None | Some n ==> Some(m+n))"

*)
end
(*>*)

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet am 2026-05-02) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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.