Changed fixity of _∎/finally, added parentheses.

Reason: A long-standing bug in Agda's operator parser has been fixed,
and some code relied on the previous behaviour.

CHANGELOG

@@ -107,6 +107,9 @@ Important changes since 0.9:
   Data.AVL, Data.AVL.IndexedMap and Data.AVL.Sets), reduce in a
   different way than they used to.
 
+* The fixity of all _∎ and finally operators was changed from infix 2
+  to infix 3.
+
 ------------------------------------------------------------------------
 -- Release notes for Agda standard library version 0.9
 ------------------------------------------------------------------------

src/Algebra/FunctionProperties.agda

@@ -51,7 +51,7 @@ Zero : A → Op₂ A → Set _
 Zero z ∙ = LeftZero z ∙ × RightZero z ∙
 
 LeftInverse : A → Op₁ A → Op₂ A → Set _
-LeftInverse e _⁻¹ _∙_ = ∀ x → (x ⁻¹ ∙ x) ≈ e
+LeftInverse e _⁻¹ _∙_ = ∀ x → ((x ⁻¹) ∙ x) ≈ e
 
 RightInverse : A → Op₁ A → Op₂ A → Set _
 RightInverse e _⁻¹ _∙_ = ∀ x → (x ∙ (x ⁻¹)) ≈ e

src/Algebra/Morphism.agda

@@ -27,7 +27,7 @@ module Definitions {f t ℓ}
   Homomorphic₀ ⟦_⟧ ∙ ∘ = ⟦ ∙ ⟧ ≈ ∘
 
   Homomorphic₁ : Morphism → Fun₁ From → Op₁ To → Set _
-  Homomorphic₁ ⟦_⟧ ∙_ ∘_ = ∀ x → ⟦ ∙ x ⟧ ≈ ∘ ⟦ x ⟧
+  Homomorphic₁ ⟦_⟧ ∙_ ∘_ = ∀ x → ⟦ ∙ x ⟧ ≈ (∘ ⟦ x ⟧)
 
   Homomorphic₂ : Morphism → Fun₂ From → Op₂ To → Set _
   Homomorphic₂ ⟦_⟧ _∙_ _∘_ =

src/Algebra/Structures.agda

@@ -308,27 +308,27 @@ record IsRing
 
     zeroˡ : LeftZero 0# _*_
     zeroˡ x = begin
-        0# * x                              ≈⟨ sym $ proj₂ +-identity _ ⟩
-       (0# * x) +            0#             ≈⟨ refl ⟨ +-cong ⟩ sym (proj₂ -‿inverse _) ⟩
-       (0# * x) + ((0# * x)  + - (0# * x))  ≈⟨ sym $ +-assoc _ _ _ ⟩
-      ((0# * x) +  (0# * x)) + - (0# * x)   ≈⟨ sym (proj₂ distrib _ _ _) ⟨ +-cong ⟩ refl ⟩
-             ((0# + 0#) * x) + - (0# * x)   ≈⟨ (proj₂ +-identity _ ⟨ *-cong ⟩ refl)
-                                                 ⟨ +-cong ⟩
-                                               refl ⟩
-                    (0# * x) + - (0# * x)   ≈⟨ proj₂ -‿inverse _ ⟩
-                             0#             ∎
+        0# * x                                ≈⟨ sym $ proj₂ +-identity _ ⟩
+       (0# * x) +            0#               ≈⟨ refl ⟨ +-cong ⟩ sym (proj₂ -‿inverse _) ⟩
+       (0# * x) + ((0# * x)  + (- (0# * x)))  ≈⟨ sym $ +-assoc _ _ _ ⟩
+      ((0# * x) +  (0# * x)) + (- (0# * x))   ≈⟨ sym (proj₂ distrib _ _ _) ⟨ +-cong ⟩ refl ⟩
+             ((0# + 0#) * x) + (- (0# * x))   ≈⟨ (proj₂ +-identity _ ⟨ *-cong ⟩ refl)
+                                                   ⟨ +-cong ⟩
+                                                 refl ⟩
+                    (0# * x) + (- (0# * x))   ≈⟨ proj₂ -‿inverse _ ⟩
+                             0#               ∎
 
     zeroʳ : RightZero 0# _*_
     zeroʳ x = begin
-      x * 0#                              ≈⟨ sym $ proj₂ +-identity _ ⟩
-      (x * 0#) + 0#                       ≈⟨ refl ⟨ +-cong ⟩ sym (proj₂ -‿inverse _) ⟩
-      (x * 0#) + ((x * 0#) + - (x * 0#))  ≈⟨ sym $ +-assoc _ _ _ ⟩
-      ((x * 0#) + (x * 0#)) + - (x * 0#)  ≈⟨ sym (proj₁ distrib _ _ _) ⟨ +-cong ⟩ refl ⟩
-      (x * (0# + 0#)) + - (x * 0#)        ≈⟨ (refl ⟨ *-cong ⟩ proj₂ +-identity _)
-                                               ⟨ +-cong ⟩
-                                             refl ⟩
-      (x * 0#) + - (x * 0#)               ≈⟨ proj₂ -‿inverse _ ⟩
-      0#                                  ∎
+      x * 0#                                ≈⟨ sym $ proj₂ +-identity _ ⟩
+      (x * 0#) + 0#                         ≈⟨ refl ⟨ +-cong ⟩ sym (proj₂ -‿inverse _) ⟩
+      (x * 0#) + ((x * 0#) + (- (x * 0#)))  ≈⟨ sym $ +-assoc _ _ _ ⟩
+      ((x * 0#) + (x * 0#)) + (- (x * 0#))  ≈⟨ sym (proj₁ distrib _ _ _) ⟨ +-cong ⟩ refl ⟩
+      (x * (0# + 0#)) + (- (x * 0#))        ≈⟨ (refl ⟨ *-cong ⟩ proj₂ +-identity _)
+                                                 ⟨ +-cong ⟩
+                                               refl ⟩
+      (x * 0#) + (- (x * 0#))               ≈⟨ proj₂ -‿inverse _ ⟩
+      0#                                    ∎
 
   isSemiringWithoutAnnihilatingZero
     : IsSemiringWithoutAnnihilatingZero ≈ _+_ _*_ 0# 1#

src/Category/Monad/Partiality.agda

@@ -329,7 +329,7 @@ module _ {a ℓ} {A : Set a} {_∼_ : A → A → Set ℓ} where
       module Pre {k}  = Preorder (preorder′ isEquivalence k)
       module S {k eq} = Setoid (setoid isEquivalence k {eq})
 
-    infix  2 _∎
+    infix  3 _∎
     infixr 2 _≡⟨_⟩_ _≅⟨_⟩_ _≳⟨_⟩_ _≈⟨_⟩_
 
     _≡⟨_⟩_ : ∀ {k} x {y z : A ⊥} → x ≡ y → Rel k y z → Rel k x z
@@ -638,7 +638,7 @@ module AlternativeEquality {a ℓ} where
   open Equality.Rel
 
   infix  4 _∣_≅P_ _∣_≳P_ _∣_≈P_
-  infix  2 _∎
+  infix  3 _∎
   infixr 2 _≡⟨_⟩_ _≅⟨_⟩_ _≳⟨_⟩_ _≳⟨_⟩≅_ _≳⟨_⟩≈_ _≈⟨_⟩≅_ _≈⟨_⟩≲_
   infixl 1 _>>=_
 

src/Category/Monad/Partiality/All.agda

@@ -68,7 +68,7 @@ module Reasoning {a p ℓ}
                  {_∼_ : A → A → Set ℓ}
                  (resp : P Respects flip _∼_) where
 
-  infix  2 finally
+  infix  3 finally
   infixr 2 _≡⟨_⟩_ _∼⟨_⟩_
 
   _≡⟨_⟩_ : ∀ x {y} → x ≡ y → All P y → All P x

src/Data/Container/Indexed/FreeMonad.agda

@@ -59,7 +59,8 @@ leaf (c , k) = do (c , return? ∘ k)
   open RawPMonad rawPMonad
 
 generic : ∀ {ℓ} {O : Set ℓ} {C : Container O O ℓ ℓ} {o}
-          (c : Command C o) → o ∈ C ⋆ ⋃[ r ∶ Response C c ] ｛ next C c r ｝
+          (c : Command C o) →
+          o ∈ C ⋆ (⋃[ r ∶ Response C c ] ｛ next C c r ｝)
 generic c = do (c , λ r → return? (r , refl))
   where
   open RawPMonad rawPMonad

src/Data/List/All/Properties.agda

@@ -108,7 +108,7 @@ private
 -- Three lemmas relating Any, All and negation.
 
 ¬Any↠All¬ : ∀ {a p} {A : Set a} {P : A → Set p} {xs} →
-            ¬ Any P xs ↠ All (¬_ ∘ P) xs
+            (¬ Any P xs) ↠ All (¬_ ∘ P) xs
 ¬Any↠All¬ {P = P} = record
   { to         = P.→-to-⟶ (to _)
   ; surjective = record
@@ -147,7 +147,7 @@ Any¬→¬All (here  ¬p) = ¬p           ∘ All.head
 Any¬→¬All (there ¬p) = Any¬→¬All ¬p ∘ All.tail
 
 Any¬⇔¬All : ∀ {a p} {A : Set a} {P : A → Set p} {xs} →
-            Decidable P → Any (¬_ ∘ P) xs ⇔ ¬ All P xs
+            Decidable P → Any (¬_ ∘ P) xs ⇔ (¬ All P xs)
 Any¬⇔¬All {P = P} dec = record
   { to   = P.→-to-⟶ Any¬→¬All
   ; from = P.→-to-⟶ (from _)

src/Data/List/Any/BagAndSetEquality.agda

@@ -113,7 +113,8 @@ concat-cong {a} {xss₁ = xss₁} {xss₂} xss₁≈xss₂ {x} =
 -- _⊛_ is a congruence.
 
 ⊛-cong : ∀ {ℓ k} {A B : Set ℓ} {fs₁ fs₂ : List (A → B)} {xs₁ xs₂} →
-         fs₁ ∼[ k ] fs₂ → xs₁ ∼[ k ] xs₂ → fs₁ ⊛ xs₁ ∼[ k ] fs₂ ⊛ xs₂
+         fs₁ ∼[ k ] fs₂ → xs₁ ∼[ k ] xs₂ →
+         (fs₁ ⊛ xs₁) ∼[ k ] (fs₂ ⊛ xs₂)
 ⊛-cong fs₁≈fs₂ xs₁≈xs₂ =
   >>=-cong fs₁≈fs₂ λ f →
   >>=-cong xs₁≈xs₂ λ x →
@@ -195,7 +196,7 @@ empty-unique {xs = _ ∷ _} ∷∼[] with ⇒→ ∷∼[] (here P.refl)
 
 ⊛-left-distributive :
   ∀ {ℓ} {A B : Set ℓ} (fs : List (A → B)) xs₁ xs₂ →
-  fs ⊛ (xs₁ ++ xs₂) ∼[ bag ] (fs ⊛ xs₁) ++ (fs ⊛ xs₂)
+  (fs ⊛ (xs₁ ++ xs₂)) ∼[ bag ] (fs ⊛ xs₁) ++ (fs ⊛ xs₂)
 ⊛-left-distributive {B = B} fs xs₁ xs₂ = begin
   fs ⊛ (xs₁ ++ xs₂)                         ≡⟨ P.refl ⟩
   (fs >>= λ f → xs₁ ++ xs₂ >>= return ∘ f)  ≡⟨ (LP.Monad.cong (P.refl {x = fs}) λ f →

src/Data/List/Any/Membership.agda

@@ -74,14 +74,14 @@ concat-∈↔ {a} {x = x} {xss} =
   where open Related.EquationalReasoning
 
 ⊛-∈↔ : ∀ {ℓ} {A B : Set ℓ} (fs : List (A → B)) {xs y} →
-       (∃₂ λ f x → f ∈ fs × x ∈ xs × y ≡ f x) ↔ y ∈ fs ⊛ xs
+       (∃₂ λ f x → f ∈ fs × x ∈ xs × y ≡ f x) ↔ y ∈ (fs ⊛ xs)
 ⊛-∈↔ {ℓ} fs {xs} {y} =
   (∃₂ λ f x → f ∈ fs × x ∈ xs × y ≡ f x)       ↔⟨ Σ.cong {a₁ = ℓ} {b₁ = ℓ} {b₂ = ℓ} Inv.id (∃∃↔∃∃ {a = ℓ} {b = ℓ} {p = ℓ} _) ⟩
   (∃ λ f → f ∈ fs × ∃ λ x → x ∈ xs × y ≡ f x)  ↔⟨ Σ.cong {a₁ = ℓ} {b₁ = ℓ} {b₂ = ℓ}
                                                          Inv.id ((_ ∎) ⟨ ×⊎.*-cong {ℓ = ℓ} ⟩ Any↔ {a = ℓ} {p = ℓ}) ⟩
   (∃ λ f → f ∈ fs × Any (_≡_ y ∘ f) xs)        ↔⟨ Any↔ {a = ℓ} {p = ℓ} ⟩
   Any (λ f → Any (_≡_ y ∘ f) xs) fs            ↔⟨ ⊛↔ ⟩
-  y ∈ fs ⊛ xs                                  ∎
+  y ∈ (fs ⊛ xs)                                ∎
   where open Related.EquationalReasoning
 
 ⊗-∈↔ : ∀ {A B : Set} {xs ys} {x : A} {y : B} →

src/Data/List/Properties.agda

@@ -414,9 +414,9 @@ module Monad where
                        (xs ∣ ys >>= f) ≡ ((xs >>= f) ∣ (ys >>= f))
   right-distributive []       ys f = refl
   right-distributive (x ∷ xs) ys f = begin
-    f x ∣ (xs ∣ ys >>= f)            ≡⟨ P.cong (_∣_ (f x)) $ right-distributive xs ys f ⟩
-    f x ∣ ((xs >>= f) ∣ (ys >>= f))  ≡⟨ P.sym $ LM.assoc (f x) _ _ ⟩
-    (f x ∣ (xs >>= f)) ∣ (ys >>= f)  ∎
+    f x ∣ (xs ∣ ys >>= f)              ≡⟨ P.cong (_∣_ (f x)) $ right-distributive xs ys f ⟩
+    f x ∣ ((xs >>= f) ∣ (ys >>= f))    ≡⟨ P.sym $ LM.assoc (f x) _ _ ⟩
+    ((f x ∣ (xs >>= f)) ∣ (ys >>= f))  ∎
     where open P.≡-Reasoning
 
   left-identity : ∀ {ℓ} {A B : Set ℓ} (x : A) (f : A → List B) →
@@ -461,15 +461,15 @@ module Applicative where
 
   -- ∅ is a left zero for _⊛_.
 
-  left-zero : ∀ {ℓ} {A B : Set ℓ} (xs : List A) → ∅ ⊛ xs ≡ ∅ {A = B}
+  left-zero : ∀ {ℓ} {A B : Set ℓ} (xs : List A) → (∅ ⊛ xs) ≡ ∅ {A = B}
   left-zero xs = begin
     ∅ ⊛ xs          ≡⟨ refl ⟩
     (∅ >>= pam xs)  ≡⟨ Monad.left-zero (pam xs) ⟩
     ∅               ∎
 
   -- ∅ is a right zero for _⊛_.
 
-  right-zero : ∀ {ℓ} {A B : Set ℓ} (fs : List (A → B)) → fs ⊛ ∅ ≡ ∅
+  right-zero : ∀ {ℓ} {A B : Set ℓ} (fs : List (A → B)) → (fs ⊛ ∅) ≡ ∅
   right-zero {ℓ} fs = begin
     fs ⊛ ∅            ≡⟨ refl ⟩
     (fs >>= pam ∅)    ≡⟨ (Monad.cong (refl {x = fs}) λ f →
@@ -481,25 +481,25 @@ module Applicative where
 
   right-distributive :
     ∀ {ℓ} {A B : Set ℓ} (fs₁ fs₂ : List (A → B)) xs →
-    (fs₁ ∣ fs₂) ⊛ xs ≡ (fs₁ ⊛ xs ∣ fs₂ ⊛ xs)
+    ((fs₁ ∣ fs₂) ⊛ xs) ≡ (fs₁ ⊛ xs ∣ fs₂ ⊛ xs)
   right-distributive fs₁ fs₂ xs = begin
     (fs₁ ∣ fs₂) ⊛ xs                     ≡⟨ refl ⟩
     (fs₁ ∣ fs₂ >>= pam xs)               ≡⟨ Monad.right-distributive fs₁ fs₂ (pam xs) ⟩
     (fs₁ >>= pam xs) ∣ (fs₂ >>= pam xs)  ≡⟨ refl ⟩
-    fs₁ ⊛ xs ∣ fs₂ ⊛ xs                  ∎
+    (fs₁ ⊛ xs ∣ fs₂ ⊛ xs)                ∎
 
   -- _⊛_ does not distribute over _∣_ from the left.
 
   private
 
     not-left-distributive :
       let fs = id ∷ id ∷ []; xs₁ = true ∷ []; xs₂ = true ∷ false ∷ [] in
-      fs ⊛ (xs₁ ∣ xs₂) ≢ (fs ⊛ xs₁ ∣ fs ⊛ xs₂)
+      (fs ⊛ (xs₁ ∣ xs₂)) ≢ (fs ⊛ xs₁ ∣ fs ⊛ xs₂)
     not-left-distributive ()
 
   -- Applicative functor laws.
 
-  identity : ∀ {a} {A : Set a} (xs : List A) → return id ⊛ xs ≡ xs
+  identity : ∀ {a} {A : Set a} (xs : List A) → (return id ⊛ xs) ≡ xs
   identity xs = begin
     return id ⊛ xs          ≡⟨ refl ⟩
     (return id >>= pam xs)  ≡⟨ Monad.left-identity id (pam xs) ⟩
@@ -519,7 +519,7 @@ module Applicative where
   composition :
     ∀ {ℓ} {A B C : Set ℓ}
     (fs : List (B → C)) (gs : List (A → B)) xs →
-    return _∘′_ ⊛ fs ⊛ gs ⊛ xs ≡ fs ⊛ (gs ⊛ xs)
+    (return _∘′_ ⊛ fs ⊛ gs ⊛ xs) ≡ (fs ⊛ (gs ⊛ xs))
   composition {ℓ} fs gs xs = begin
     return _∘′_ ⊛ fs ⊛ gs ⊛ xs                      ≡⟨ refl ⟩
     (return _∘′_ >>= pam fs >>= pam gs >>= pam xs)  ≡⟨ Monad.cong (Monad.cong (Monad.left-identity _∘′_ (pam fs))
@@ -538,15 +538,15 @@ module Applicative where
     fs ⊛ (gs ⊛ xs)                                  ∎
 
   homomorphism : ∀ {ℓ} {A B : Set ℓ} (f : A → B) x →
-                 return f ⊛ return x ≡ return (f x)
+                 (return f ⊛ return x) ≡ return (f x)
   homomorphism f x = begin
     return f ⊛ return x            ≡⟨ refl ⟩
     (return f >>= pam (return x))  ≡⟨ Monad.left-identity f (pam (return x)) ⟩
     pam (return x) f               ≡⟨ Monad.left-identity x (return ∘ f) ⟩
     return (f x)                   ∎
 
   interchange : ∀ {ℓ} {A B : Set ℓ} (fs : List (A → B)) {x} →
-                fs ⊛ return x ≡ return (λ f → f x) ⊛ fs
+                (fs ⊛ return x) ≡ (return (λ f → f x) ⊛ fs)
   interchange fs {x} = begin
     fs ⊛ return x                    ≡⟨ refl ⟩
     (fs >>= pam (return x))          ≡⟨ (Monad.cong (refl {x = fs}) λ f →

src/Data/Plus.agda

@@ -37,7 +37,7 @@ finally _ _ = id
 syntax finally x y x∼⁺y = x ∼⁺⟨ x∼⁺y ⟩∎ y ∎
 
 infixr 2 _∼⁺⟨_⟩_
-infix  2 finally
+infix  3 finally
 
 -- Map.
 

src/Function/Related.agda

@@ -269,7 +269,7 @@ module EquationalReasoning where
   sym {equivalence} = Eq.sym
   sym {bijection}   = Inv.sym
 
-  infix  2 _∎
+  infix  3 _∎
   infixr 2 _∼⟨_⟩_ _↔⟨_⟩_ _↔⟨⟩_ _≡⟨_⟩_
 
   _∼⟨_⟩_ : ∀ {k x y z} (X : Set x) {Y : Set y} {Z : Set z} →

src/Relation/Binary/HeterogeneousEquality.agda

@@ -170,7 +170,7 @@ module ≅-Reasoning where
   -- heterogeneous equalities, hence the code duplication here.
 
   infix  4 _IsRelatedTo_
-  infix  2 _∎
+  infix  3 _∎
   infixr 2 _≅⟨_⟩_ _≡⟨_⟩_ _≡⟨⟩_
   infix  1 begin_
 

src/Relation/Binary/PreorderReasoning.agda

@@ -31,7 +31,7 @@ module Relation.Binary.PreorderReasoning
 open Preorder P
 
 infix  4 _IsRelatedTo_
-infix  2 _∎
+infix  3 _∎
 infixr 2 _∼⟨_⟩_ _≈⟨_⟩_ _≈⟨⟩_
 infix  1 begin_
 

src/Relation/Binary/SetoidReasoning.agda

@@ -31,7 +31,7 @@ module Relation.Binary.SetoidReasoning where
 
 infix 1 begin⟨_⟩_
 infixr 2 _≈⟨_⟩_ _≡⟨_⟩_
-infix 2 _∎
+infix 3 _∎
 
 begin⟨_⟩_ : ∀ {c l} (S : Setoid c l) → {x y : Carrier S} → _IsRelatedTo_ S x y → _≈_ S x y
 begin⟨_⟩_ S p = EqR.begin_ S p