From 9f631b114e1cdcbaf3610eefd6f9fd7baeeda0c1 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 25 May 2020 22:17:11 +0100 Subject: Continuing work on proving specification --- src/common/Monad.v | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'src/common') diff --git a/src/common/Monad.v b/src/common/Monad.v index 773918a..8517186 100644 --- a/src/common/Monad.v +++ b/src/common/Monad.v @@ -39,4 +39,10 @@ Module MonadExtra(M : Monad). ret (r::rs) end. + Fixpoint collectlist {A : Type} (f : A -> mon unit) (l : list A) {struct l} : mon unit := + match l with + | nil => ret tt + | x::xs => do _ <- f x; collectlist f xs + end. + End MonadExtra. -- cgit