Skip to content
Snippets Groups Projects
Commit 187db929 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Something close to non-expansiveness of is_Some.

parent a121e077
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 2 additions and 0 deletions
modures/option.v
+ 2
− 0
View file @ 187db929
...@@ -49,6 +49,8 @@ Proof. by intros ?; inversion_clear 1; constructor; apply timeless. Qed. ...@@ -49,6 +49,8 @@ Proof. by intros ?; inversion_clear 1; constructor; apply timeless. Qed.
Instance option_fmap_ne `{Dist A, Dist B} (f : A → B) n: Instance option_fmap_ne `{Dist A, Dist B} (f : A → B) n:
Proper (dist n ==> dist n) f → Proper (dist n==>dist n) (fmap (M:=option) f). Proper (dist n ==> dist n) f → Proper (dist n==>dist n) (fmap (M:=option) f).
Proof. by intros Hf; destruct 1; constructor; apply Hf. Qed. Proof. by intros Hf; destruct 1; constructor; apply Hf. Qed.
Instance is_Some_ne `{Dist A} : Proper (dist (S n) ==> iff) (@is_Some A).
Proof. intros n; inversion_clear 1; split; eauto. Qed.
(* CMRA *) (* CMRA *)
Instance option_valid `{Valid A} : Valid (option A) := λ mx, Instance option_valid `{Valid A} : Valid (option A) := λ mx,
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment