From b06d11d9e12cae00475e8f9a5f69d42cf34ae729 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 11 Feb 2019 16:34:03 -0800 Subject: Add Option.{lift,map,combine}, List.Option.lift These will be useful for extending the AST with `option` types. --- src/Util/OptionList.v | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'src/Util/OptionList.v') diff --git a/src/Util/OptionList.v b/src/Util/OptionList.v index c2157346e..4b88dd9a3 100644 --- a/src/Util/OptionList.v +++ b/src/Util/OptionList.v @@ -25,6 +25,11 @@ Module Option. | x :: xs => (x <- x; @bind_list A B xs (fun xs => f (x :: xs))) end%option%list. + Definition lift {A} (ls : list (option A)) : option (list A) + := fold_right (fun x xs => x <- x; xs <- xs; Some (x :: xs))%option + (Some nil) + ls. + Module Export Notations. Notation "A <-- X ; B" := (bind_list X (fun A => B%option)) : option_scope. End Notations. -- cgit v1.2.3