diff options
| author | Joris | 2020-08-09 14:44:02 +0200 |
|---|---|---|
| committer | Joris | 2020-08-09 14:44:02 +0200 |
| commit | 225068497c5fd41da12030a6bbf58a0fc9c294d0 (patch) | |
| tree | a2432c1c8004a3e5897a4a9b445e256a3ca6c651 /src/Lib/Option.ml | |
| parent | ad6abcd5fc5e4e66062c8a01b511a1bd4bda2e94 (diff) | |
Import from CSV
Diffstat (limited to 'src/Lib/Option.ml')
| -rw-r--r-- | src/Lib/Option.ml | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/Lib/Option.ml b/src/Lib/Option.ml new file mode 100644 index 0000000..1158b96 --- /dev/null +++ b/src/Lib/Option.ml @@ -0,0 +1,9 @@ +let withDefault default opt = + match opt with + | Some v -> v + | None -> default + +let map f opt = + match opt with + | Some v -> Some (f v) + | None -> None |