fix atomic update trailing spaces

iris/bi/lib/atomic.v

@@ -113,7 +113,7 @@ Notation "'AU' '<<' ∀ x1 .. xn , α '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'C
                         ) .. )
   )
   (at level 20, Eo, Ei, α, β, Φ at level 200, x1 binder, xn binder, y1 binder, yn binder,
-   format "'[hv   ' 'AU'  '<<'  '[' ∀  x1  ..  xn ,  '/' α  ']' '>>'  '/' @  '[' Eo ,  '/' Ei  ']' '/' '<<'  '[' ∃  y1  ..  yn ,  '/' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
+   format "'[hv   ' 'AU'  '<<'  '[' ∀  x1  ..  xn ,  '/' α  ']' '>>'  '/' @  '[' Eo ,  '/' Ei ']'  '/' '<<'  '[' ∃  y1  ..  yn ,  '/' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
 
 Notation "'AU' '<<' ∀ x1 .. xn , α '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
   (atomic_update (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
@@ -127,7 +127,7 @@ Notation "'AU' '<<' ∀ x1 .. xn , α '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :
                        λ x1, .. (λ xn, tele_app (TT:=TeleO) Φ%I) .. )
   )
   (at level 20, Eo, Ei, α, β, Φ at level 200, x1 binder, xn binder,
-   format "'[hv   ' 'AU'  '<<'  '[' ∀  x1  ..  xn ,  '/' α  ']' '>>'  '/' @  '[' Eo ,  '/' Ei  ']' '/' '<<'  '[' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
+   format "'[hv   ' 'AU'  '<<'  '[' ∀  x1  ..  xn ,  '/' α  ']' '>>'  '/' @  '[' Eo ,  '/' Ei ']'  '/' '<<'  '[' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
 
 Notation "'AU' '<<' α '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM' Φ '>>'" :=
   (atomic_update (TA:=TeleO)
@@ -142,7 +142,7 @@ Notation "'AU' '<<' α '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM' Φ '>>'" :
                                 (λ y1, .. (λ yn, Φ%I) ..))
   )
   (at level 20, Eo, Ei, α, β, Φ at level 200, y1 binder, yn binder,
-   format "'[hv   ' 'AU'  '<<'  '[' α  ']' '>>'  '/' @  '[' Eo ,  '/' Ei  ']' '/' '<<'  '[' ∃  y1  ..  yn ,  '/' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
+   format "'[hv   ' 'AU'  '<<'  '[' α  ']' '>>'  '/' @  '[' Eo ,  '/' Ei ']'  '/' '<<'  '[' ∃  y1  ..  yn ,  '/' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
 
 Notation "'AU' '<<' α '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
   (atomic_update (TA:=TeleO) (TB:=TeleO) Eo Ei
@@ -151,7 +151,7 @@ Notation "'AU' '<<' α '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
                  (tele_app (TT:=TeleO) $ tele_app (TT:=TeleO) Φ%I)
   )
   (at level 20, Eo, Ei, α, β, Φ at level 200,
-   format "'[hv   ' 'AU'  '<<'  '[' α  ']' '>>'  '/' @  '[' Eo ,  '/' Ei  ']' '/' '<<'  '[' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
+   format "'[hv   ' 'AU'  '<<'  '[' α  ']' '>>'  '/' @  '[' Eo ,  '/' Ei ']'  '/' '<<'  '[' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
 
 (** Notation: Atomic accessors *)
 Notation "'AACC' '<<' ∀ x1 .. xn , α , 'ABORT' P '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM' Φ '>>'" :=
@@ -173,7 +173,7 @@ Notation "'AACC' '<<' ∀ x1 .. xn , α , 'ABORT' P '>>' @ Eo , Ei '<<' ∃ y1 .
                      ) .. )
   )
   (at level 20, Eo, Ei, α, P, β, Φ at level 200, x1 binder, xn binder, y1 binder, yn binder,
-   format "'[hv     ' 'AACC'  '<<'  '[' ∀  x1  ..  xn ,  '/' α ,  '/' ABORT  P  ']' '>>'  '/' @  '[' Eo ,  '/' Ei  ']' '/' '<<'  '[' ∃  y1  ..  yn ,  '/' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
+   format "'[hv     ' 'AACC'  '<<'  '[' ∀  x1  ..  xn ,  '/' α ,  '/' ABORT  P  ']' '>>'  '/' @  '[' Eo ,  '/' Ei ']'  '/' '<<'  '[' ∃  y1  ..  yn ,  '/' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
 
 Notation "'AACC' '<<' ∀ x1 .. xn , α , 'ABORT' P '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
   (atomic_acc (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
@@ -188,7 +188,7 @@ Notation "'AACC' '<<' ∀ x1 .. xn , α , 'ABORT' P '>>' @ Eo , Ei '<<' β , 'CO
                         λ x1, .. (λ xn, tele_app (TT:=TeleO) Φ%I) .. )
   )
   (at level 20, Eo, Ei, α, P, β, Φ at level 200, x1 binder, xn binder,
-   format "'[hv     ' 'AACC'  '<<'  '[' ∀  x1  ..  xn ,  '/' α ,  '/' ABORT  P  ']' '>>'  '/' @  '[' Eo ,  '/' Ei  ']' '/' '<<'  '[' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
+   format "'[hv     ' 'AACC'  '<<'  '[' ∀  x1  ..  xn ,  '/' α ,  '/' ABORT  P  ']' '>>'  '/' @  '[' Eo ,  '/' Ei ']'  '/' '<<'  '[' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
 
 Notation "'AACC' '<<' α , 'ABORT' P '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM' Φ '>>'" :=
   (atomic_acc (TA:=TeleO)
@@ -204,7 +204,7 @@ Notation "'AACC' '<<' α , 'ABORT' P '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'CO
                         (λ y1, .. (λ yn, Φ%I) ..))
   )
   (at level 20, Eo, Ei, α, P, β, Φ at level 200, y1 binder, yn binder,
-   format "'[hv     ' 'AACC'  '<<'  '[' α ,  '/' ABORT  P  ']' '>>'  '/' @  '[' Eo ,  '/' Ei  ']' '/' '<<'  '[' ∃  y1  ..  yn ,  '/' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
+   format "'[hv     ' 'AACC'  '<<'  '[' α ,  '/' ABORT  P  ']' '>>'  '/' @  '[' Eo ,  '/' Ei ']'  '/' '<<'  '[' ∃  y1  ..  yn ,  '/' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
 
 Notation "'AACC' '<<' α , 'ABORT' P '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
   (atomic_acc (TA:=TeleO)
@@ -216,7 +216,7 @@ Notation "'AACC' '<<' α , 'ABORT' P '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
                  (tele_app (TT:=TeleO) $ tele_app (TT:=TeleO) Φ%I)
   )
   (at level 20, Eo, Ei, α, P, β, Φ at level 200,
-   format "'[hv     ' 'AACC'  '<<'  '[' α ,  '/' ABORT  P  ']' '>>'  '/' @  '[' Eo ,  '/' Ei  ']' '/' '<<'  '[' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
+   format "'[hv     ' 'AACC'  '<<'  '[' α ,  '/' ABORT  P  ']' '>>'  '/' @  '[' Eo ,  '/' Ei ']'  '/' '<<'  '[' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
 
 (** Lemmas about AU *)
 Section lemmas.

tests/atomic.ref

@@ -10,7 +10,7 @@
   "Hl" : l ↦ v
   --------------------------------------∗
   AACC << ∀ (v0 : val) (q : dfrac), l ↦{q} v0, ABORT l ↦ v >>
-       @ ⊤ ∖ ∅, ∅ 
+       @ ⊤ ∖ ∅, ∅
        << l ↦{q} v0, COMM Q -∗ Q >>
 "non_laterable"
      : string
@@ -25,7 +25,7 @@
   "HP" : ▷ P
   --------------------------------------∗
   AACC << ∀ (v : val) (q : dfrac), l ↦{q} v, ABORT ▷ P >>
-       @ ⊤ ∖ ∅, ∅ 
+       @ ⊤ ∖ ∅, ∅
        << l ↦{q} v, COMM True >>
 1 goal
   
@@ -38,7 +38,7 @@
   "HP" : ▷ P
   --------------------------------------∗
   AACC << ∀ (v : val) (q : dfrac), l ↦{q} v, ABORT ▷ P >>
-       @ ⊤ ∖ ∅, ∅ 
+       @ ⊤ ∖ ∅, ∅
        << l ↦{q} v, COMM True >>
 "printing"
      : string
@@ -68,9 +68,9 @@
   ============================
   _ : AACC << ∀ x : val, P x,
               ABORT AU << ∀ x : val, P x >>
-                       @ ⊤ ∖ ∅, ∅ 
+                       @ ⊤ ∖ ∅, ∅
                        << ∃ y : val, P y, COMM Φ #() >> >>
-           @ ⊤ ∖ ∅, ∅ 
+           @ ⊤ ∖ ∅, ∅
            << ∃ y : val, P y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
@@ -100,9 +100,9 @@
   ============================
   _ : AACC << ∀ x : val, l ↦ x,
               ABORT AU << ∀ x : val, l ↦ x >>
-                       @ ⊤ ∖ ∅, ∅ 
+                       @ ⊤ ∖ ∅, ∅
                        << l ↦ x, COMM Φ #() >> >>
-           @ ⊤ ∖ ∅, ∅ 
+           @ ⊤ ∖ ∅, ∅
            << l ↦ x, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
@@ -132,9 +132,9 @@
   ============================
   _ : AACC << l ↦ #(),
               ABORT AU << l ↦ #() >>
-                       @ ⊤ ∖ ∅, ∅ 
+                       @ ⊤ ∖ ∅, ∅
                        << ∃ y : val, l ↦ y, COMM Φ #() >> >>
-           @ ⊤ ∖ ∅, ∅ 
+           @ ⊤ ∖ ∅, ∅
            << ∃ y : val, l ↦ y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
@@ -164,7 +164,7 @@
   ============================
   _ : AACC << l ↦ #(),
               ABORT AU << l ↦ #() >> @ ⊤ ∖ ∅, ∅ << l ↦ #(), COMM Φ #() >> >>
-           @ ⊤ ∖ ∅, ∅ 
+           @ ⊤ ∖ ∅, ∅
            << l ↦ #(), COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
@@ -187,7 +187,7 @@
   Φ : language.val heap_lang → iProp Σ
   ============================
   "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x >>
-            @ ⊤ ∖ ∅, ∅ 
+            @ ⊤ ∖ ∅, ∅
             << ∃ y : val, l ↦ y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
@@ -208,7 +208,7 @@
   Φ : language.val heap_lang → iProp Σ
   ============================
   "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>
-            @ ⊤ ∖ ∅, ∅ 
+            @ ⊤ ∖ ∅, ∅
             << ∃ y : val, l ↦ y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
@@ -230,7 +230,7 @@
   Φ : language.val heap_lang → iProp Σ
   ============================
   _ : AU << ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>
-         @ ⊤ ∖ ∅, ∅ 
+         @ ⊤ ∖ ∅, ∅
          << ∃ yyyy : val, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗
             l ↦ xx, COMM Φ #() >>
   --------------------------------------∗
@@ -252,7 +252,7 @@
   Φ : language.val heap_lang → iProp Σ
   ============================
   "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>
-            @ ⊤ ∖ ∅, ∅ 
+            @ ⊤ ∖ ∅, ∅
             << l ↦ x, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
@@ -275,7 +275,7 @@
   Φ : language.val heap_lang → iProp Σ
   ============================
   "AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>
-            @ ⊤ ∖ ∅, ∅ 
+            @ ⊤ ∖ ∅, ∅
             << ∃ y : val, l ↦ y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
@@ -298,7 +298,7 @@
   Φ : language.val heap_lang → iProp Σ
   ============================
   "AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>
-            @ ⊤ ∖ ∅, ∅ 
+            @ ⊤ ∖ ∅, ∅
             << l ↦ #(), COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
@@ -321,7 +321,7 @@
   Φ : language.val heap_lang → iProp Σ
   ============================
   "AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>
-            @ ⊤ ∖ ∅, ∅ 
+            @ ⊤ ∖ ∅, ∅
             << l ↦ yyyy, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
@@ -345,7 +345,7 @@
   Φ : language.val heap_lang → iProp Σ
   ============================
   "AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>
-            @ ⊤ ∖ ∅, ∅ 
+            @ ⊤ ∖ ∅, ∅
             << l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗
                l ↦ xx, COMM Φ #() >>
   --------------------------------------∗
@@ -362,7 +362,7 @@
   "AU" : ∃ x : val, P x ∗
            (P x ={∅,⊤}=∗
             AU << ∀ x0 : val, P x0 >>
-               @ ⊤ ∖ ∅, ∅ 
+               @ ⊤ ∖ ∅, ∅
                << ∃ y : val, P y, COMM Φ #() >>)
            ∧ (∀ x0 : val, P x0 ={∅,⊤}=∗ Φ #())
   --------------------------------------∗