Commit ee8b3ce8 by Robbert Krebbers

### Notation for auth that does not conflict with composition of functions.

parent 2523157b
 ... @@ -6,8 +6,8 @@ Record auth (A : Type) : Type := Auth { authoritative : excl A ; own : A }. ... @@ -6,8 +6,8 @@ Record auth (A : Type) : Type := Auth { authoritative : excl A ; own : A }. Arguments Auth {_} _ _. Arguments Auth {_} _ _. Arguments authoritative {_} _. Arguments authoritative {_} _. Arguments own {_} _. Arguments own {_} _. Notation "∘ x" := (Auth ExclUnit x) (at level 20). Notation "◯ x" := (Auth ExclUnit x) (at level 20). Notation "∙ x" := (Auth (Excl x) ∅) (at level 20). Notation "● x" := (Auth (Excl x) ∅) (at level 20). (* COFE *) (* COFE *) Instance auth_equiv `{Equiv A} : Equiv (auth A) := λ x y, Instance auth_equiv `{Equiv A} : Equiv (auth A) := λ x y, ... @@ -122,7 +122,7 @@ Proof. ... @@ -122,7 +122,7 @@ Proof. split; [apply (ra_empty_valid (A:=A))|]. split; [apply (ra_empty_valid (A:=A))|]. by intros x; constructor; simpl; rewrite (left_id _ _). by intros x; constructor; simpl; rewrite (left_id _ _). Qed. Qed. Lemma auth_frag_op `{CMRA A} a b : ∘(a ⋅ b) ≡ ∘a ⋅ ∘b. Lemma auth_frag_op `{CMRA A} a b : ◯ (a ⋅ b) ≡ ◯ a ⋅ ◯ b. Proof. done. Qed. Proof. done. Qed. (* Functor *) (* Functor *) ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!