diff options
author | Yann Herklotz <git@yannherklotz.com> | 2021-02-16 14:11:32 +0000 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2021-02-16 14:11:32 +0000 |
commit | 6a395495bd35bb7d4d2cc7d3271c9b588d466594 (patch) | |
tree | 0fcc285046352b9f677454eac3224ce5a90ba48e /src/common/Vericertlib.v | |
parent | 5f1e7aa8fbc4a0e04d0b137410c13f3d8da4d987 (diff) | |
parent | b5c79cb4913087a0e4b577b5dff616fc88ee938b (diff) | |
download | vericert-6a395495bd35bb7d4d2cc7d3271c9b588d466594.tar.gz vericert-6a395495bd35bb7d4d2cc7d3271c9b588d466594.zip |
Merge branch 'michalis' of https://github.com/mpardalos/vericert into michalis-merge
Diffstat (limited to 'src/common/Vericertlib.v')
-rw-r--r-- | src/common/Vericertlib.v | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/common/Vericertlib.v b/src/common/Vericertlib.v index f2754be..a0d2af1 100644 --- a/src/common/Vericertlib.v +++ b/src/common/Vericertlib.v @@ -230,6 +230,15 @@ Definition join {A : Type} (a : option (option A)) : option A := | Some a' => a' end. +Fixpoint map_option {A B : Type} (f : A -> option B) (l : list A) : list B := + match l with + | nil => nil + | x::xs => match f x with + | None => map_option f xs + | Some x' => x'::map_option f xs + end + end. + Module Notation. Notation "'do' X <- A ; B" := (bind A (fun X => B)) (at level 200, X ident, A at level 100, B at level 200). |