diff options
Diffstat (limited to 'src/Util/OptionList.v')
-rw-r--r-- | src/Util/OptionList.v | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/src/Util/OptionList.v b/src/Util/OptionList.v new file mode 100644 index 000000000..57cc52f06 --- /dev/null +++ b/src/Util/OptionList.v @@ -0,0 +1,20 @@ +Require Import Crypto.Util.Notations. + +Module Option. + 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. +End Option. |