SHARE
TWEET

Untitled

a guest Jul 19th, 2019 59 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.
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
 
Top