Changeset 1551 for src/utilities/option.ma

Timestamp:

Nov 24, 2011, 11:52:52 AM (9 years ago)

Author:

campbell

Message:

Functions to translate between back-end and front-end values.

File:

• src/utilities/option.ma (modified) (1 diff)

src/utilities/option.ma

@@ -16 +16 @@
 ] qed.
 
+definition option_map_def : ∀A,B:Type[0]. (A → B) → B → option A → B ≝
+λA,B,f,d,o. match o with [ None ⇒ d | Some a ⇒ f a ].
+
 lemma refute_none_by_refl : ∀A,B:Type[0]. ∀P:A → B. ∀Q:B → Type[0]. ∀x:option A. ∀H:x = None ? → False.
   (∀v. x = Some ? v → Q (P v)) →