| 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.thySprache: 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 (*>*)
¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet am 2026-06-10) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-06-09