From 5c76a00e565b86c132269b187731e8f55f473dd4 Mon Sep 17 00:00:00 2001
From: Simon Friis Vindum <simonfv@gmail.com>
Date: Mon, 21 Nov 2022 14:49:33 +0100
Subject: [PATCH] Add Fractional and AsFractional instance for embed
---
iris/bi/lib/fractional.v | 8 ++++++++
1 file changed, 8 insertions(+)
diff --git a/iris/bi/lib/fractional.v b/iris/bi/lib/fractional.v
index 2303c1c31..05917ee57 100644
--- a/iris/bi/lib/fractional.v
+++ b/iris/bi/lib/fractional.v
@@ -87,6 +87,14 @@ Section fractional.
rewrite !assoc. f_equiv. by rewrite comm.
Qed.
+ Global Instance fractional_embed `{!BiEmbed PROP PROP'} Φ :
+ Fractional Φ → Fractional (λ q, ⎡ Φ q ⎤ : PROP')%I.
+ Proof. intros ???. by rewrite fractional embed_sep. Qed.
+
+ Global Instance as_fractional_embed `{!BiEmbed PROP PROP'} P Φ q :
+ AsFractional P Φ q → AsFractional (⎡ P ⎤) (λ q, ⎡ Φ q ⎤)%I q.
+ Proof. split; [by rewrite ->!as_fractional | apply _]. Qed.
+
Global Instance fractional_big_sepL {A} (l : list A) Ψ :
(∀ k x, Fractional (Ψ k x)) →
Fractional (PROP:=PROP) (λ q, [∗ list] k↦x ∈ l, Ψ k x q)%I.
--
GitLab