Commit 617a69b4 authored by Robbert Krebbers's avatar Robbert Krebbers

Rename fmap_Some_equiv' → fmap_Some_equiv_1.

We typically use the _1 and _2 suffix to denote individual directions
of a lemmas that is a biimplication.
parent 22fac635
Pipeline #3271 passed with stage
in 10 minutes and 52 seconds
......@@ -190,10 +190,10 @@ Proof.
- intros ?%symmetry%equiv_None. done.
- intros (? & ? & ?). done.
Lemma fmap_Some_equiv' {A B} `{Equiv B} `{!Equivalence (() : relation B)}
Lemma fmap_Some_equiv_1 {A B} `{Equiv B} `{!Equivalence (() : relation B)}
  • A heads-up for this would have been nice, lambdaRust used this function.

Please register or sign in to reply
(f : A B) mx y :
f <$> mx Some y x, mx = Some x y f x.
Proof. intros. apply fmap_Some_equiv. done. Qed.
Proof. by rewrite fmap_Some_equiv. Qed.
Lemma fmap_None {A B} (f : A B) mx : f <$> mx = None mx = None.
Proof. by destruct mx. Qed.
Lemma option_fmap_id {A} (mx : option A) : id <$> mx = mx.
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment