From 1a019465f66800a3018216efe47c787022700d6b Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Sun, 7 Jul 2019 22:11:57 +0200 Subject: [PATCH] fix list variable name --- theories/list.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/theories/list.v b/theories/list.v index 33d15d5..c1c2ede 100644 --- a/theories/list.v +++ b/theories/list.v @@ -911,17 +911,17 @@ Section find. Lemma list_find_fmap {B : Type} (f : B → A) (l : list B) : list_find P (f <\$> l) = prod_map id f <\$> list_find (P ∘ f) l. Proof. - induction l as [|x y IH]; [done|]. simpl. + induction l as [|x l IH]; [done|]. simpl. case_decide; [done|]. - change (list_fmap B A f y) with (f <\$> y). (* FIXME it simplified too much *) - rewrite IH. by destruct (list_find (P ∘ f) y). + change (list_fmap B A f l) with (f <\$> l). (* FIXME it simplified too much *) + rewrite IH. by destruct (list_find (P ∘ f) l). Qed. Lemma list_find_proper (Q : A → Prop) `{∀ x, Decision (Q x)} l : (∀ x, P x ↔ Q x) → list_find P l = list_find Q l. Proof. - intros HPQ. induction l as [|x y IH]; [done|]. simpl. + intros HPQ. induction l as [|x l IH]; [done|]. simpl. erewrite decide_iff by done. by rewrite IH. Qed. End find. -- 2.24.1