Commit 1a019465 by Ralf Jung

### fix list variable name

parent 05bf88b7
 ... @@ -911,17 +911,17 @@ Section find. ... @@ -911,17 +911,17 @@ Section find. Lemma list_find_fmap {B : Type} (f : B → A) (l : list B) : 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. list_find P (f <\$> l) = prod_map id f <\$> list_find (P ∘ f) l. Proof. Proof. induction l as [|x y IH]; [done|]. simpl. induction l as [|x l IH]; [done|]. simpl. case_decide; [done|]. case_decide; [done|]. change (list_fmap B A f y) with (f <\$> y). (* FIXME it simplified too much *) change (list_fmap B A f l) with (f <\$> l). (* FIXME it simplified too much *) rewrite IH. by destruct (list_find (P ∘ f) y). rewrite IH. by destruct (list_find (P ∘ f) l). Qed. Qed. Lemma list_find_proper (Q : A → Prop) `{∀ x, Decision (Q x)} l : Lemma list_find_proper (Q : A → Prop) `{∀ x, Decision (Q x)} l : (∀ x, P x ↔ Q x) → (∀ x, P x ↔ Q x) → list_find P l = list_find Q l. list_find P l = list_find Q l. Proof. 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. erewrite decide_iff by done. by rewrite IH. Qed. Qed. End find. End find. ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!