1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
19 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
21 (* Questo materiale fa parte della tesi: *)
22 (* "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale" *)
24 (* data ultima modifica 15/11/2007 *)
25 (* ********************************************************************** *)
27 include "freescale/bool.ma".
33 ninductive option (A:Type) : Type ≝
35 | Some : A → option A.
37 ndefinition option_ind : ΠA:Type.ΠP:option A → Prop.P (None A) → (Πa:A.P (Some A a)) → Πo:option A.P o ≝
38 λA:Type.λP:option A → Prop.λp:P (None A).λf:Πa:A.P (Some A a).λo:option A.
39 match o with [ None ⇒ p | Some (a:A) ⇒ f a ].
41 ndefinition option_rec : ΠA:Type.ΠP:option A → Set.P (None A) → (Πa:A.P (Some A a)) → Πo:option A.P o ≝
42 λA:Type.λP:option A → Set.λp:P (None A).λf:Πa:A.P (Some A a).λo:option A.
43 match o with [ None ⇒ p | Some (a:A) ⇒ f a ].
45 ndefinition option_rect : ΠA:Type.ΠP:option A → Type.P (None A) → (Πa:A.P (Some A a)) → Πo:option A.P o ≝
46 λA:Type.λP:option A → Type.λp:P (None A).λf:Πa:A.P (Some A a).λo:option A.
47 match o with [ None ⇒ p | Some (a:A) ⇒ f a ].
49 ndefinition eq_option ≝
50 λT.λo1,o2:option T.λf:T → T → bool.
52 [ None ⇒ match o2 with [ None ⇒ true | Some _ ⇒ false ]
53 | Some x1 ⇒ match o2 with [ None ⇒ false | Some x2 ⇒ f x1 x2 ]
56 (* option map = match ... with [ None ⇒ None ? | Some .. ⇒ .. ] *)
58 λT1,T2:Type.λt:option T1.λf:T1 → option T2.
59 match t with [ None ⇒ None ? | Some x ⇒ (f x) ].