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)}
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›).
, 🍋‹nat› extended with $\infty$ can be modeled by type
🍋‹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}.
›
(*<*)
(*
definition infplus :: "nat option \<Rightarrow> nat option \<Rightarrow> nat option" where
"infplus x y \<equiv> case x of None \<Rightarrow> None
| Some m \<Rightarrow> (case y of None \<Rightarrow> None | Some n \<Rightarrow> Some(m+n))"

*)
end
(*>*)

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.2 Sekunden ¤

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.