diff options
| -rw-r--r-- | _CoqProject | 1 | ||||
| -rw-r--r-- | src/Util/Option.v | 17 | ||||
| -rw-r--r-- | src/Util/OptionList.v | 20 |
3 files changed, 21 insertions, 17 deletions
diff --git a/_CoqProject b/_CoqProject index 6352367df..4adfef055 100644 --- a/_CoqProject +++ b/_CoqProject @@ -6471,6 +6471,7 @@ src/Util/NatUtil.v src/Util/Notations.v src/Util/NumTheoryUtil.v src/Util/Option.v +src/Util/OptionList.v src/Util/ParseTaps.v src/Util/PartiallyReifiedProp.v src/Util/Pointed.v diff --git a/src/Util/Option.v b/src/Util/Option.v index e14ad263e..b9e64910c 100644 --- a/src/Util/Option.v +++ b/src/Util/Option.v @@ -18,23 +18,6 @@ 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 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. |