From 5634e2a85b20e8c209e4796905679dc06f62001b Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 12 Jul 2022 15:24:12 -0400
Subject: [PATCH] support fractional framing of ghost_var (like mapsto)

---
 iris/base_logic/lib/ghost_var.v | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/iris/base_logic/lib/ghost_var.v b/iris/base_logic/lib/ghost_var.v
index 937d9ac56..448b0d3f3 100644
--- a/iris/base_logic/lib/ghost_var.v
+++ b/iris/base_logic/lib/ghost_var.v
@@ -90,4 +90,10 @@ Section lemmas.
     ghost_var γ (1/2) b ∗ ghost_var γ (1/2) b.
   Proof. iApply ghost_var_update_2. apply Qp_half_half. Qed.
 
+  (** Framing support *)
+  Global Instance frame_ghost_var p γ a q1 q2 RES :
+    FrameFractionalHyps p (ghost_var γ q1 a) (λ q, ghost_var γ q a)%I RES q1 q2 →
+    Frame p (ghost_var γ q1 a) (ghost_var γ q2 a) RES | 5.
+  Proof. apply: frame_fractional. Qed.
+
 End lemmas.
-- 
GitLab