From 232489491f580251a0b5f397054f4307b132f002 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 8 Jun 2022 15:34:46 +0200
Subject: [PATCH] =?UTF-8?q?Add=20`Absorbing`=20instances=20for=20`[?=
 =?UTF-8?q?=E2=88=A7=20list]`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 iris/bi/big_op.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index e31916ec5..f5f422eef 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -1014,6 +1014,13 @@ Section and_list.
     Proper (Forall2 (⊢) ==> (⊢)) (big_opL (@bi_and PROP) (λ _ P, P)).
   Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
 
+  Global Instance big_andL_nil_absorbing Φ :
+    Absorbing ([∧ list] k↦x ∈ [], Φ k x).
+  Proof. simpl; apply _. Qed.
+  Global Instance big_andL_absorbing Φ l :
+    (∀ k x, Absorbing (Φ k x)) → Absorbing ([∧ list] k↦x ∈ l, Φ k x).
+  Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
+
   Global Instance big_andL_nil_persistent Φ :
     Persistent ([∧ list] k↦x ∈ [], Φ k x).
   Proof. simpl; apply _. Qed.
-- 
GitLab