Commit 6b6e322c by Ralf Jung

### auth.v: reduce noise by putting definitions in a section

parent 13011e3c
 ... @@ -10,14 +10,14 @@ Class AuthInG Λ Σ (i : gid) (A : cmraT) `{Empty A} := { ... @@ -10,14 +10,14 @@ Class AuthInG Λ Σ (i : gid) (A : cmraT) `{Empty A} := { (* TODO: Once we switched to RAs, it is no longer necessary to remember that a is (* TODO: Once we switched to RAs, it is no longer necessary to remember that a is constantly valid. *) constantly valid. *) Definition auth_inv {Λ Σ A} (i : gid) `{AuthInG Λ Σ i A} Section definitions. (γ : gname) (φ : A → iPropG Λ Σ) : iPropG Λ Σ := Context {Λ Σ A} (i : gid) `{AuthInG Λ Σ i A} (γ : gname). (∃ a, (■ ✓ a ∧ own i γ (● a)) ★ φ a)%I. Definition auth_inv (φ : A → iPropG Λ Σ) : iPropG Λ Σ := Definition auth_own {Λ Σ A} (i : gid) `{AuthInG Λ Σ i A} (∃ a, (■ ✓ a ∧ own i γ (● a)) ★ φ a)%I. (γ : gname) (a : A) : iPropG Λ Σ := own i γ (◯ a). Definition auth_own (a : A) : iPropG Λ Σ := own i γ (◯ a). Definition auth_ctx {Λ Σ A} (i : gid) `{AuthInG Λ Σ i A} Definition auth_ctx (N : namespace) (φ : A → iPropG Λ Σ) : iPropG Λ Σ := (γ : gname) (N : namespace) (φ : A → iPropG Λ Σ) : iPropG Λ Σ := inv N (auth_inv φ). inv N (auth_inv i γ φ). End definitions. Instance: Params (@auth_inv) 7. Instance: Params (@auth_inv) 7. Instance: Params (@auth_own) 7. Instance: Params (@auth_own) 7. Instance: Params (@auth_ctx) 8. Instance: Params (@auth_ctx) 8. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!