Skip to content
GitLab

`excl_auth` camera

Merged Robbert Krebbers requested to merge robbert/excl_auth into master

At various places we use auth (option (excl A)), and @jihgfee proposed that it is useful to have a common abstraction for it. So, here it goes!

Definition excl_authR (A : ofeT) : cmraT :=
  authR (optionUR (exclR A)).

Definition excl_auth_auth {A : ofeT} (a : A) : excl_authR A :=
  ● (Some (Excl a)).
Definition excl_auth_frag {A : ofeT} (a : A) : excl_authR A :=
  ◯ (Some (Excl a)).

Notation "●E a" := (excl_auth_auth a) (at level 10).
Notation "◯E a" := (excl_auth_frag a) (at level 10).

The MR proves a bunch of useful lemmas about this abstraction. The notations and lemmas follow the style in the file frac_auth.

Edited by Robbert Krebbers