Added option_map

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6903 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 6 insertions, 0 deletions

diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index d10bea6055..48f5c14975 100755
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -61,6 +61,12 @@ Inductive option (A:Set) : Set :=
 
 Implicit Arguments None [A].
 
+Definition option_map (A B:Set) (f:A->B) o :=
+  match o with
+  | Some a => Some (f a)
+  | None => None
+  end.
+
 (** [sum A B], equivalently [A + B], is the disjoint sum of [A] and [B] *)
 (* Syntax defined in Specif.v *)
 Inductive sum (A B:Set) : Set :=