From ec34ec23058bc5708c43604b680ae788e3563a86 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 31 Mar 2005 11:39:08 +0000
Subject: Added option_map

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6903 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Init/Datatypes.v | 6 ++++++
 1 file changed, 6 insertions(+)

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 :=
-- 
cgit v1.2.3