Commit 4e43a270 authored by Ralf Jung's avatar Ralf Jung

comment on the validity trick in auth

parent cc1191b9
......@@ -8,6 +8,8 @@ Class AuthInG Λ Σ (i : gid) (A : cmraT) `{Empty A} := {
auth_timeless (a : A) :> Timeless a;
}.
(* TODO: Once we switched to RAs, it is no longer necessary to remember that a is
constantly valid. *)
Definition auth_inv {Λ Σ A} (i : gid) `{AuthInG Λ Σ i A}
(γ : gname) (φ : A iPropG Λ Σ) : iPropG Λ Σ := ( a, (■✓a own i γ ( a)) φ a)%I.
Definition auth_own {Λ Σ A} (i : gid) `{AuthInG Λ Σ i A}
......
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