diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-05-25 22:17:11 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-05-25 22:17:11 +0100 |
| commit | 9f631b114e1cdcbaf3610eefd6f9fd7baeeda0c1 (patch) | |
| tree | 51ea6969859aad9c1a9b27ba5ef7e82ca426fd61 /src/common | |
| parent | 0c5ca8061a887f397991e62b580d5fc2f6484336 (diff) | |
| download | vericert-9f631b114e1cdcbaf3610eefd6f9fd7baeeda0c1.tar.gz vericert-9f631b114e1cdcbaf3610eefd6f9fd7baeeda0c1.zip | |
Continuing work on proving specification
Diffstat (limited to 'src/common')
| -rw-r--r-- | src/common/Monad.v | 6 |
1 files changed, 6 insertions, 0 deletions
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. |