From b65cf6799cf278fc79d7f36a587fc944d0d2bcd9 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 11 Jun 2018 23:16:55 +0200
Subject: [PATCH] fix format spacing for texan triples
---
theories/program_logic/weakestpre.v | 40 ++++++++++++++---------------
1 file changed, 20 insertions(+), 20 deletions(-)
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 139a5d78b..724bfc033 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -89,93 +89,93 @@ Notation "'{{{' P } } } e @ s ; E {{{ x .. y , 'RET' pat ; Q } } }" :=
(□ ∀ Φ,
P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ s; E {{ Φ }})%I
(at level 20, x closed binder, y closed binder,
- format "{{{ P } } } e @ s ; E {{{ x .. y , RET pat ; Q } } }") : bi_scope.
+ format "{{{ P } } } e @ s ; E {{{ x .. y , RET pat ; Q } } }") : bi_scope.
Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' 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 , RET pat ; Q } } }") : bi_scope.
+ format "{{{ P } } } e @ E {{{ x .. y , RET pat ; Q } } }") : bi_scope.
Notation "'{{{' P } } } e @ E ? {{{ x .. y , 'RET' 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 , RET pat ; Q } } }") : bi_scope.
+ format "{{{ P } } } e @ E ? {{{ x .. y , RET pat ; Q } } }") : bi_scope.
Notation "'{{{' P } } } e {{{ x .. y , 'RET' 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 , RET pat ; Q } } }") : bi_scope.
+ format "{{{ P } } } e {{{ x .. y , RET pat ; Q } } }") : bi_scope.
Notation "'{{{' P } } } e ? {{{ x .. y , 'RET' 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 , RET pat ; Q } } }") : bi_scope.
+ format "{{{ P } } } e ? {{{ x .. y , RET pat ; Q } } }") : bi_scope.
Notation "'{{{' P } } } e @ s ; E {{{ 'RET' pat ; Q } } }" :=
(□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ s; E {{ Φ }})%I
(at level 20,
- format "{{{ P } } } e @ s ; E {{{ RET pat ; Q } } }") : bi_scope.
+ format "{{{ P } } } e @ s ; E {{{ RET pat ; Q } } }") : bi_scope.
Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" :=
(□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E {{ Φ }})%I
(at level 20,
- format "{{{ P } } } e @ E {{{ RET pat ; Q } } }") : bi_scope.
+ format "{{{ P } } } e @ E {{{ RET pat ; Q } } }") : bi_scope.
Notation "'{{{' P } } } e @ E ? {{{ 'RET' pat ; Q } } }" :=
(□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E ?{{ Φ }})%I
(at level 20,
- format "{{{ P } } } e @ E ? {{{ RET pat ; Q } } }") : bi_scope.
+ format "{{{ P } } } e @ E ? {{{ RET pat ; Q } } }") : bi_scope.
Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }" :=
(□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e {{ Φ }})%I
(at level 20,
- format "{{{ P } } } e {{{ RET pat ; Q } } }") : bi_scope.
+ format "{{{ P } } } e {{{ RET pat ; Q } } }") : bi_scope.
Notation "'{{{' P } } } e ? {{{ 'RET' pat ; Q } } }" :=
(□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e ?{{ Φ }})%I
(at level 20,
- format "{{{ P } } } e ? {{{ RET pat ; Q } } }") : bi_scope.
+ format "{{{ P } } } e ? {{{ RET pat ; Q } } }") : bi_scope.
Notation "'{{{' P } } } e @ s ; E {{{ x .. y , 'RET' pat ; Q } } }" :=
(∀ Φ : _ → uPred _,
P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ s; E {{ Φ }})
(at level 20, x closed binder, y closed binder,
- format "{{{ P } } } e @ s ; E {{{ x .. y , RET pat ; Q } } }") : stdpp_scope.
+ format "{{{ P } } } e @ s ; E {{{ x .. y , RET pat ; Q } } }") : stdpp_scope.
Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" :=
(∀ Φ : _ → uPred _,
P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E {{ Φ }})
(at level 20, x closed binder, y closed binder,
- format "{{{ P } } } e @ E {{{ x .. y , RET pat ; Q } } }") : stdpp_scope.
+ format "{{{ P } } } e @ E {{{ x .. y , RET pat ; Q } } }") : stdpp_scope.
Notation "'{{{' P } } } e @ E ? {{{ x .. y , 'RET' pat ; Q } } }" :=
(∀ Φ : _ → uPred _,
P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E ?{{ Φ }})
(at level 20, x closed binder, y closed binder,
- format "{{{ P } } } e @ E ? {{{ x .. y , RET pat ; Q } } }") : stdpp_scope.
+ format "{{{ P } } } e @ E ? {{{ x .. y , RET pat ; Q } } }") : stdpp_scope.
Notation "'{{{' P } } } e {{{ x .. y , 'RET' pat ; Q } } }" :=
(∀ Φ : _ → uPred _,
P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e {{ Φ }})
(at level 20, x closed binder, y closed binder,
- format "{{{ P } } } e {{{ x .. y , RET pat ; Q } } }") : stdpp_scope.
+ format "{{{ P } } } e {{{ x .. y , RET pat ; Q } } }") : stdpp_scope.
Notation "'{{{' P } } } e ? {{{ x .. y , 'RET' pat ; Q } } }" :=
(∀ Φ : _ → uPred _,
P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e ?{{ Φ }})
(at level 20, x closed binder, y closed binder,
- format "{{{ P } } } e ? {{{ x .. y , RET pat ; Q } } }") : stdpp_scope.
+ format "{{{ P } } } e ? {{{ x .. y , RET pat ; Q } } }") : stdpp_scope.
Notation "'{{{' P } } } e @ s ; E {{{ 'RET' pat ; Q } } }" :=
(∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ s; E {{ Φ }})
(at level 20,
- format "{{{ P } } } e @ s ; E {{{ RET pat ; Q } } }") : stdpp_scope.
+ format "{{{ P } } } e @ s ; E {{{ RET pat ; Q } } }") : stdpp_scope.
Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" :=
(∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E {{ Φ }})
(at level 20,
- format "{{{ P } } } e @ E {{{ RET pat ; Q } } }") : stdpp_scope.
+ format "{{{ P } } } e @ E {{{ RET pat ; Q } } }") : stdpp_scope.
Notation "'{{{' P } } } e @ E ? {{{ 'RET' pat ; Q } } }" :=
(∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E ?{{ Φ }})
(at level 20,
- format "{{{ P } } } e @ E ? {{{ RET pat ; Q } } }") : stdpp_scope.
+ format "{{{ P } } } e @ E ? {{{ RET pat ; Q } } }") : stdpp_scope.
Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }" :=
(∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e {{ Φ }})
(at level 20,
- format "{{{ P } } } e {{{ RET pat ; Q } } }") : stdpp_scope.
+ format "{{{ P } } } e {{{ RET pat ; Q } } }") : stdpp_scope.
Notation "'{{{' P } } } e ? {{{ 'RET' pat ; Q } } }" :=
(∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e ?{{ Φ }})
(at level 20,
- format "{{{ P } } } e ? {{{ RET pat ; Q } } }") : stdpp_scope.
+ format "{{{ P } } } e ? {{{ RET pat ; Q } } }") : stdpp_scope.
Section wp.
Context `{irisG Λ Σ}.
--
GitLab