diff options
Diffstat (limited to 'theories')
| -rwxr-xr-x | theories/Init/Datatypes.v | 6 |
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 := |