From 543b1b707d79d7b2385c108d1916079696feefd7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 22 Dec 2015 13:18:34 +0100
Subject: [PATCH] Definition of big conjunction.

---
 modures/logic.v | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/modures/logic.v b/modures/logic.v
index f4bdf9136..5417e2a36 100644
--- a/modures/logic.v
+++ b/modures/logic.v
@@ -202,6 +202,11 @@ Notation "✓" := uPred_valid (at level 1) : uPred_scope.
 Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P → Q) ∧ (Q → P))%I.
 Infix "↔" := uPred_iff : uPred_scope.
 
+Fixpoint uPred_big_and {M} (Ps : list (uPred M)) :=
+  match Ps with [] => True | P :: Ps => P ∧ uPred_big_and Ps end%I.
+Fixpoint uPred_big_sep {M} (Ps : list (uPred M)) :=
+  match Ps with [] => True | P :: Ps => P ★ uPred_big_sep Ps end%I.
+
 Class TimelessP {M} (P : uPred M) := timelessP x n : ✓{1} x → P 1 x → P n x.
 
 Module uPred. Section uPred_logic.
-- 
GitLab