Commit 1a47979d authored by Jonas Kastberg Hinrichsen's avatar Jonas Kastberg Hinrichsen
Browse files

WIP

parent 605562ba
......@@ -71,7 +71,11 @@ Section stype_ofe.
+ intros st. induction st; constructor; repeat intro; auto.
+ intros st1 st2. induction 1; constructor; repeat intro; auto.
symmetry; auto.
+ admit.
+ intros st1 st2 st3 H1 H2. revert H1. revert st1.
induction 1.
* inversion H2. constructor.
* inversion H2. eauto.
admit.
- intros n st1 st2. induction 1; constructor; auto.
Admitted.
Canonical Structure stypeC : ofeT := OfeT (stype A) stype_ofe_mixin.
......@@ -111,7 +115,7 @@ Lemma stype_map_ext {A} {B : ofeT} (f g : A → B) (st : stype A) :
( x, f x g x) stype_map f st stype_map g st.
Proof.
intros Hf. induction st; simpl.
Admitted.
Admitted.
Instance styope_map_ne {A B : ofeT} (f : A B) n:
Proper (dist n ==> dist n) f Proper (dist n ==> dist n) (stype_map f).
Proof.
......
Markdown is supported
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