(**************************************************************************)
(* ********************************************************************** *)
-(* Progetto FreeScale *)
+(* Progetto FreeScale *)
(* *)
-(* Sviluppato da: *)
-(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
(* *)
-(* Questo materiale fa parte della tesi: *)
-(* "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale" *)
-(* *)
-(* data ultima modifica 15/11/2007 *)
(* ********************************************************************** *)
include "freescale/bool.ma".
None : option A
| Some : A → option A.
-ndefinition option_ind : ΠA:Type.ΠP:option A → Prop.P (None A) → (Πa:A.P (Some A a)) → Πop:option A.P op ≝
-λA:Type.λP:option A → Prop.λp:P (None A).λf:Πa:A.P (Some A a).λop:option A.
- match op with [ None ⇒ p | Some (a:A) ⇒ f a ].
-
-ndefinition option_rec : ΠA:Type.ΠP:option A → Set.P (None A) → (Πa:A.P (Some A a)) → Πop:option A.P op ≝
-λA:Type.λP:option A → Set.λp:P (None A).λf:Πa:A.P (Some A a).λop:option A.
- match op with [ None ⇒ p | Some (a:A) ⇒ f a ].
-
-ndefinition option_rect : ΠA:Type.ΠP:option A → Type.P (None A) → (Πa:A.P (Some A a)) → Πop:option A.P op ≝
-λA:Type.λP:option A → Type.λp:P (None A).λf:Πa:A.P (Some A a).λop:option A.
- match op with [ None ⇒ p | Some (a:A) ⇒ f a ].
-
ndefinition eq_option ≝
λT.λop1,op2:option T.λf:T → T → bool.
match op1 with