| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Doc/Tutorial/Misc/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 1 kB |
|
Quelle Option2.thy Sprache: 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.14 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28