From 54252fbc10eaa88941ec1e157ce2c2e575e42604 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Fri, 23 Apr 2021 14:27:46 +0200 Subject: [PATCH] Fix comment. Thanks @mpu. --- theories/list.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/list.v b/theories/list.v index e0c5fdeb..4a0321ab 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 -- GitLab