Commit c136a440 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

No longer let `to_agree` require the carrier to be an OFE.

parent 6c7b99c2
...@@ -34,6 +34,9 @@ Arguments agree_car {_} _. ...@@ -34,6 +34,9 @@ Arguments agree_car {_} _.
Arguments agree_not_nil {_} _. Arguments agree_not_nil {_} _.
Local Coercion agree_car : agree >-> list. Local Coercion agree_car : agree >-> list.
Definition to_agree {A} (a : A) : agree A :=
{| agree_car := [a]; agree_not_nil := eq_refl |}.
Lemma elem_of_agree {A} (x : agree A) : a, a agree_car x. Lemma elem_of_agree {A} (x : agree A) : a, a agree_car x.
Proof. destruct x as [[|a ?] ?]; set_solver+. Qed. Proof. destruct x as [[|a ?] ?]; set_solver+. Qed.
Lemma agree_eq {A} (x y : agree A) : agree_car x = agree_car y x = y. Lemma agree_eq {A} (x y : agree A) : agree_car x = agree_car y x = y.
...@@ -156,9 +159,6 @@ Proof. ...@@ -156,9 +159,6 @@ Proof.
apply discrete_iff_0; auto. apply discrete_iff_0; auto.
Qed. Qed.
Program Definition to_agree (a : A) : agree A :=
{| agree_car := [a]; agree_not_nil := eq_refl |}.
Global Instance to_agree_ne : NonExpansive to_agree. Global Instance to_agree_ne : NonExpansive to_agree.
Proof. Proof.
intros n a1 a2 Hx; split=> b /=; intros n a1 a2 Hx; split=> b /=;
......
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