diff --git a/theories/list.v b/theories/list.v index e0c5fdebbad3c3223a123ccd0362c515632ad831..4a0321abe5f41998ec8a7c0bc0a86f54377087bd 100644 --- a/theories/list.v +++ b/theories/list.v @@ -221,7 +221,7 @@ Definition mapM `{MBind M, MRet M} {A B} (f : A → M B) : list A → M (list B) fix go l := match l with [] => mret [] | x :: l => y ↠f x; k ↠go l; mret (y :: k) end. -(** We define stronger variants of map and fold that allow the mapped +(** We define stronger variants of the map function that allow the mapped function to use the index of the elements. *) Fixpoint imap {A B} (f : nat → A → B) (l : list A) : list B := match l with