Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: xop721.cob Sprache: Isabelle

Original von: Isabelle^©

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

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

datatype 'a option = None | Some 'a

text\<open>\noindent
Frequently one needs to add a distinguished element to some existing type.
For example, type \<open>t option\<close> can model the result of a computation that
may either terminate with an error (represented by \<^const>\<open>None\<close>) or return
some value \<^term>\<open>v\<close> (represented by \<^term>\<open>Some v\<close>).
Similarly, \<^typ>\<open>nat\<close> extended with $\infty$ can be modeled by type
\<^typ>\<open>nat option\<close>. In both cases one could define a new datatype with
customized constructors like \<^term>\<open>Error\<close> and \<^term>\<open>Infinity\<close>,
but it is often simpler to use \<open>option\<close>. For an application see
\S\ref{sec:Trie}.
\<close>
(*<*)
(*
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
(*>*)

¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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 ist noch experimentell.