add texan triples in uPred_scope

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 {{ Φ }})