aboutsummaryrefslogtreecommitdiffstats
path: root/src/common/Monad.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/common/Monad.v')
-rw-r--r--src/common/Monad.v3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/common/Monad.v b/src/common/Monad.v
index ece047c..b7d97a1 100644
--- a/src/common/Monad.v
+++ b/src/common/Monad.v
@@ -66,4 +66,7 @@ Module MonadExtra(M : Monad).
| x::xs => do _ <- f x; collectlist f xs
end.
+ Definition mfold_left {A B} (f: A -> B -> mon A) (l: list B) (s: mon A): mon A :=
+ fold_left (fun a b => do a' <- a; f a' b) l s.
+
End MonadExtra.