diff options
author | Jason Gross <jagro@google.com> | 2018-06-04 17:03:11 -0400 |
---|---|---|
committer | Jason Gross <jagro@google.com> | 2018-06-04 17:03:11 -0400 |
commit | 88d9d2c6e02c6a29e25fbfa90e92c5416a9c13d4 (patch) | |
tree | 7831cc566bc488965c1dc6297930905ca389f69b /src/Util | |
parent | e19e55d62139056c2c2455b8075d845d88f4e93e (diff) |
Add Option.List.map
Diffstat (limited to 'src/Util')
-rw-r--r-- | src/Util/Option.v | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/src/Util/Option.v b/src/Util/Option.v index b9e64910c..e14ad263e 100644 --- a/src/Util/Option.v +++ b/src/Util/Option.v @@ -18,6 +18,23 @@ Module Export Notations. End Notations. Local Open Scope option_scope. +Module List. + Section map. + Context {A B} + (f : A -> option B). + + Fixpoint map (ls : list A) : list B + := match ls with + | nil => nil + | cons x xs + => match f x with + | Some fx => fx :: map xs + | None => map xs + end + end. + End map. +End List. + Section Relations. Definition option_eq {A} eq (x y : option A) := match x with |