From 94c07daa48c9bb151124a0ad24b15e919f3d7463 Mon Sep 17 00:00:00 2001
From: Michael Sammler <noreply@sammler.me>
Date: Thu, 23 Apr 2020 12:47:01 +0200
Subject: [PATCH] fix imap_seq and imap_seq0 to make them useful

---
 theories/list_numbers.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/list_numbers.v b/theories/list_numbers.v
index cde4f53e..7393cd62 100644
--- a/theories/list_numbers.v
+++ b/theories/list_numbers.v
@@ -38,14 +38,14 @@ Section seq.
   Qed.
   Lemma fmap_S_seq j n : S <$> seq j n = seq (S j) n.
   Proof. apply (fmap_add_seq 1). Qed.
-  Lemma imap_seq {A} (l : list A) (g : nat → A) i :
+  Lemma imap_seq {A B} (l : list A) (g : nat → B) i :
     imap (λ j _, g (i + j)) l = g <$> seq i (length l).
   Proof.
     revert i. induction l as [|x l IH]; [done|].
     csimpl. intros n. rewrite <-IH, <-plus_n_O. f_equal.
     apply imap_ext; simpl; auto with lia.
   Qed.
-  Lemma imap_seq_0 {A} (l : list A) (g : nat → A) :
+  Lemma imap_seq_0 {A B} (l : list A) (g : nat → B) :
     imap (λ j _, g j) l = g <$> seq 0 (length l).
   Proof. rewrite (imap_ext _ (λ i o, g (0 + i))); [|done]. apply imap_seq. Qed.
   Lemma lookup_seq_lt j n i : i < n → seq j n !! i = Some (j + i).
-- 
GitLab