(* ********************************************************************** *)
(* Progetto FreeScale *)
(* *)
-(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppo: 2008-2010 *)
(* *)
(* ********************************************************************** *)
| Some : A → option A.
ndefinition eq_option ≝
-λT.λop1,op2:option T.λf:T → T → bool.
+λT.λf:T → T → bool.λop1,op2:option T.
match op1 with
[ None ⇒ match op2 with [ None ⇒ true | Some _ ⇒ false ]
| Some x1 ⇒ match op2 with [ None ⇒ false | Some x2 ⇒ f x1 x2 ]