From 90ba4346bfb49a078f18085553d35f145f922c04 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 27 Oct 2016 11:09:42 +0200
Subject: [PATCH] add texan triples in uPred_scope

---
 program_logic/weakestpre.v | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index 9f7b8af60..4865f544b 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -51,6 +51,25 @@ Notation "'WP' e {{ v , Q } }" := (wp ⊤ e%E (λ v, Q))
    format "'WP'  e  {{  v ,  Q  } }") : uPred_scope.
 
 (* Texan triples *)
+Notation "'{{{' P } } } e {{{ x .. y ; pat , Q } } }" :=
+  (□ ∀ Φ,
+      P ★ ▷ (∀ x, .. (∀ y, Q -★ Φ pat%V) .. ) -★ WP e {{ Φ }})%I
+    (at level 20, x closed binder, y closed binder,
+     format "{{{  P  } } }  e  {{{ x .. y ;  pat ,  Q } } }") : uPred_scope.
+Notation "'{{{' P } } } e @ E {{{ x .. y ; pat , Q } } }" :=
+  (□ ∀ Φ,
+      P ★ ▷ (∀ x, .. (∀ y, Q -★ Φ pat%V) .. ) -★ WP e @ E {{ Φ }})%I
+    (at level 20, x closed binder, y closed binder,
+     format "{{{  P  } } }  e  @  E  {{{ x .. y ;  pat ,  Q } } }") : uPred_scope.
+Notation "'{{{' P } } } e {{{ ; pat , Q } } }" :=
+  (□ ∀ Φ, P ★ ▷ (Q -★ Φ pat%V) -★ WP e {{ Φ }})%I
+    (at level 20,
+     format "{{{  P  } } }  e  {{{ ; pat ,  Q } } }") : uPred_scope.
+Notation "'{{{' P } } } e @ E {{{ ; pat , Q } } }" :=
+  (□ ∀ Φ, P ★ ▷ (Q -★ Φ pat%V) -★ WP e @ E {{ Φ }})%I
+    (at level 20,
+     format "{{{  P  } } }  e  @  E  {{{ ; pat ,  Q } } }") : uPred_scope.
+
 Notation "'{{{' P } } } e {{{ x .. y ; pat , Q } } }" :=
   (∀ Φ : _ → uPred _,
       P ★ ▷ (∀ x, .. (∀ y, Q -★ Φ pat%V) .. ) ⊢ WP e {{ Φ }})
-- 
GitLab