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 *)
18 (* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
21 (* ********************************************************************** *)
23 include "freescale/bool.ma".
29 ninductive option (A:Type) : Type ≝
31 | Some : A → option A.
33 ndefinition option_ind : ΠA:Type.ΠP:option A → Prop.P (None A) → (Πa:A.P (Some A a)) → Πop:option A.P op ≝
34 λA:Type.λP:option A → Prop.λp:P (None A).λf:Πa:A.P (Some A a).λop:option A.
35 match op with [ None ⇒ p | Some (a:A) ⇒ f a ].
37 ndefinition option_rec : ΠA:Type.ΠP:option A → Set.P (None A) → (Πa:A.P (Some A a)) → Πop:option A.P op ≝
38 λA:Type.λP:option A → Set.λp:P (None A).λf:Πa:A.P (Some A a).λop:option A.
39 match op with [ None ⇒ p | Some (a:A) ⇒ f a ].
41 ndefinition option_rect : ΠA:Type.ΠP:option A → Type.P (None A) → (Πa:A.P (Some A a)) → Πop:option A.P op ≝
42 λA:Type.λP:option A → Type.λp:P (None A).λf:Πa:A.P (Some A a).λop:option A.
43 match op with [ None ⇒ p | Some (a:A) ⇒ f a ].
45 ndefinition eq_option ≝
46 λT.λop1,op2:option T.λf:T → T → bool.
48 [ None ⇒ match op2 with [ None ⇒ true | Some _ ⇒ false ]
49 | Some x1 ⇒ match op2 with [ None ⇒ false | Some x2 ⇒ f x1 x2 ]
52 (* option map = match ... with [ None ⇒ None ? | Some .. ⇒ .. ] *)
54 λT1,T2:Type.λt:option T1.λf:T1 → option T2.
55 match t with [ None ⇒ None ? | Some x ⇒ (f x) ].