Commit 31598b91 authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coq

parents 4b81074e ac6f5d18
...@@ -26,11 +26,10 @@ Proof. ...@@ -26,11 +26,10 @@ Proof.
Thus Ag(T) is not necessarily complete. Thus Ag(T) is not necessarily complete.
*) *)
Record agree (A : Type) : Type := Agree { Record agree (A : Type) : Type := {
agree_car : list A; agree_car : list A;
agree_not_nil : bool_decide (agree_car = []) = false agree_not_nil : bool_decide (agree_car = []) = false
}. }.
Arguments Agree {_} _ _.
Arguments agree_car {_} _. Arguments agree_car {_} _.
Arguments agree_not_nil {_} _. Arguments agree_not_nil {_} _.
Local Coercion agree_car : agree >-> list. Local Coercion agree_car : agree >-> list.
...@@ -82,7 +81,7 @@ Instance agree_validN : ValidN (agree A) := λ n x, ...@@ -82,7 +81,7 @@ Instance agree_validN : ValidN (agree A) := λ n x,
Instance agree_valid : Valid (agree A) := λ x, n, {n} x. Instance agree_valid : Valid (agree A) := λ x, n, {n} x.
Program Instance agree_op : Op (agree A) := λ x y, Program Instance agree_op : Op (agree A) := λ x y,
Agree (agree_car x ++ agree_car y) _. {| agree_car := agree_car x ++ agree_car y |}.
Next Obligation. by intros [[|??]] y. Qed. Next Obligation. by intros [[|??]] y. Qed.
Instance agree_pcore : PCore (agree A) := Some. Instance agree_pcore : PCore (agree A) := Some.
......
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