Commit a19d201e authored by Ralf Jung's avatar Ralf Jung
Browse files

use sections to scope options

parent c654a73e
...@@ -39,29 +39,30 @@ Notation "x ≼{ n } y" := (includedN n x y) ...@@ -39,29 +39,30 @@ Notation "x ≼{ n } y" := (includedN n x y)
Instance: Params (@includedN) 4. Instance: Params (@includedN) 4.
Hint Extern 0 (_ {_} _) => reflexivity. Hint Extern 0 (_ {_} _) => reflexivity.
Set Primitive Projections. Section mixin.
Record CMRAMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, ValidN A} := { Local Set Primitive Projections.
(* setoids *) Record CMRAMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, ValidN A} := {
mixin_cmra_op_ne (x : A) : NonExpansive (op x); (* setoids *)
mixin_cmra_pcore_ne n x y cx : mixin_cmra_op_ne (x : A) : NonExpansive (op x);
x {n} y pcore x = Some cx cy, pcore y = Some cy cx {n} cy; mixin_cmra_pcore_ne n x y cx :
mixin_cmra_validN_ne n : Proper (dist n ==> impl) (validN n); x {n} y pcore x = Some cx cy, pcore y = Some cy cx {n} cy;
(* valid *) mixin_cmra_validN_ne n : Proper (dist n ==> impl) (validN n);
mixin_cmra_valid_validN x : x n, {n} x; (* valid *)
mixin_cmra_validN_S n x : {S n} x {n} x; mixin_cmra_valid_validN x : x n, {n} x;
(* monoid *) mixin_cmra_validN_S n x : {S n} x {n} x;
mixin_cmra_assoc : Assoc () (); (* monoid *)
mixin_cmra_comm : Comm () (); mixin_cmra_assoc : Assoc () ();
mixin_cmra_pcore_l x cx : pcore x = Some cx cx x x; mixin_cmra_comm : Comm () ();
mixin_cmra_pcore_idemp x cx : pcore x = Some cx pcore cx Some cx; mixin_cmra_pcore_l x cx : pcore x = Some cx cx x x;
mixin_cmra_pcore_mono x y cx : mixin_cmra_pcore_idemp x cx : pcore x = Some cx pcore cx Some cx;
x y pcore x = Some cx cy, pcore y = Some cy cx cy; mixin_cmra_pcore_mono x y cx :
mixin_cmra_validN_op_l n x y : {n} (x y) {n} x; x y pcore x = Some cx cy, pcore y = Some cy cx cy;
mixin_cmra_extend n x y1 y2 : mixin_cmra_validN_op_l n x y : {n} (x y) {n} x;
{n} x x {n} y1 y2 mixin_cmra_extend n x y1 y2 :
z1 z2, x z1 z2 z1 {n} y1 z2 {n} y2 {n} x x {n} y1 y2
}. z1 z2, x z1 z2 z1 {n} y1 z2 {n} y2
Unset Primitive Projections. }.
End mixin.
(** Bundeled version *) (** Bundeled version *)
Structure cmraT := CMRAT' { Structure cmraT := CMRAT' {
......
...@@ -33,13 +33,14 @@ Tactic Notation "ofe_subst" := ...@@ -33,13 +33,14 @@ Tactic Notation "ofe_subst" :=
| H:@dist ?A ?d ?n _ ?x |- _ => symmetry in H;setoid_subst_aux (@dist A d n) x | H:@dist ?A ?d ?n _ ?x |- _ => symmetry in H;setoid_subst_aux (@dist A d n) x
end. end.
Set Primitive Projections. Section mixin.
Record OfeMixin A `{Equiv A, Dist A} := { Local Set Primitive Projections.
mixin_equiv_dist x y : x y n, x {n} y; Record OfeMixin A `{Equiv A, Dist A} := {
mixin_dist_equivalence n : Equivalence (dist n); mixin_equiv_dist x y : x y n, x {n} y;
mixin_dist_S n x y : x {S n} y x {n} y mixin_dist_equivalence n : Equivalence (dist n);
}. mixin_dist_S n x y : x {S n} y x {n} y
Unset Primitive Projections. }.
End mixin.
(** Bundeled version *) (** Bundeled version *)
Structure ofeT := OfeT' { Structure ofeT := OfeT' {
......
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