Advertisement
Guest User

Untitled

a guest
Jul 19th, 2019
82
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. From iris.base_logic.lib Require Export invariants.
  2. From iris.proofmode Require Import tactics.
  3. From iris.heap_lang Require Import proofmode notation lang.
  4. From iris.program_logic Require Export atomic.
  5.  
  6. From iris.algebra Require Import cmra agree auth excl.
  7.  
  8. Section test.
  9.  
  10. Definition za := (authR (prodUR
  11. (prodUR
  12. (optionUR (exclR unitO))
  13. (optionUR (exclR unitO)))
  14. (optionUR (agreeR (boolO))))).
  15.  
  16. Class kkG Σ := Kk { kk_sG :> inG Σ za }.
  17. Definition kkΣ : gFunctors := #[GFunctor za].
  18.  
  19. Instance subG_kkΣ {Σ} : subG kkΣ Σ -> kkG Σ.
  20. Proof. solve_inG. Qed.
  21.  
  22. Context `{heapG Σ} `{kkG Σ}.
  23. Global Instance passed_persistent γ: Persistent (own γ (◯((None, None), Some (to_agree true)))).
  24. Proof. typeclasses eauto 10. Qed.
Advertisement
Advertisement
Advertisement
RAW Paste Data Copied
Advertisement