diff options
| -rw-r--r-- | src/common/NonEmpty.v | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/src/common/NonEmpty.v b/src/common/NonEmpty.v index 9cb7650..923a637 100644 --- a/src/common/NonEmpty.v +++ b/src/common/NonEmpty.v @@ -70,6 +70,12 @@ Fixpoint of_list {A} (l: list A): option (non_empty A) := | nil => None end. +Fixpoint of_list_def {A} (d: A) (l: list A): non_empty A := + match l with + | a::b => a ::| of_list_def d b + | nil => singleton d + end. + Fixpoint replace {A} (f: A -> A -> bool) (a b: A) (l: non_empty A) := match l with | a' ::| l' => if f a a' then b ::| replace f a b l' else a' ::| replace f a b l' @@ -108,3 +114,15 @@ Fixpoint filter {A: Type} (f: A -> bool) (l: non_empty A) : option (non_empty A) match filter f b with Some x => Some (a ::| x) | None => Some (singleton a) end else filter f b end. + +Fixpoint fold_left {A B} (f: A -> B -> A) (l: non_empty B) (a: A) {struct l} : A := + match l with + | singleton a' => f a a' + | b ::| t => fold_left f t (f a b) + end. + +Fixpoint fold_right {A B} (f: B -> A -> A) (a: A) (l: non_empty B) {struct l} : A := + match l with + | singleton a' => f a' a + | b ::| t => fold_right f (f b a) t + end. |