Add new fixities (#2116)

Co-authored-by: Sofia El Boufi--Crouzet <[email protected]>

Author: 2 people

CHANGELOG.md

@@ -120,6 +120,34 @@ Bug-fixes
   infixl  6 _+ℤ_                                             (Relation.Binary.HeterogeneousEquality.Quotients.Examples)
   infix   4 _≉_ _≈ᵢ_ _≤ᵢ_                                    (Relation.Binary.Indexed.Homogeneous.Bundles)
   infixr  5 _∷ᴹ_ _∷⁻¹ᴹ_                                      (Text.Regex.Search)
+  infixr  4 _,_                                              (Data.Refinement)
+  infixr  4 _,_                                              (Data.Container.Relation.Binary.Pointwise)
+  infixr  4 _,_                                              (Data.Tree.AVL.Value)
+  infixr  4 _,_                                              (Foreign.Haskell.Pair)
+  infixr  4 _,_                                              (Reflection.AnnotatedAST)
+  infixr  4 _,_                                              (Reflection.AST.Traversal)
+  infixl  6.5 _P′_ _P_ _C′_ _C_                              (Data.Nat.Combinatorics.Base)
+  infixl  1 _>>=-cong_ _≡->>=-cong_                          (Effect.Monad.Partiality)
+  infixl  1 _?>=′_                                           (Effect.Monad.Predicate)
+  infixl  1 _>>=-cong_ _>>=-congP_                           (Effect.Monad.Partiality.All)
+  infix   4 _∈FV_                                            (Reflection.AST.DeBruijn)
+  infixr  9 _;_                                              (Relation.Binary.Construct.Composition)
+  infixl  6 _+²_                                             (Relation.Binary.HeterogeneousEquality.Quotients.Examples)
+  infixr -1 _atₛ_                                             (Relation.Binary.Indexed.Heterogeneous.Construct.At)
+  infixr -1 _atₛ_                                             (Relation.Binary.Indexed.Homogeneous.Construct.At)
+  infix   4 _∈_ _∉_                                          (Relation.Unary.Indexed)
+  infixr  9 _⍮_                                              (Relation.Unary.PredicateTransformer)
+  infix   8 ∼_                                               (Relation.Unary.PredicateTransformer)
+  infix   2 _×?_ _⊙?_                                        (Relation.Unary.Properties)
+  infix   10 _~?                                             (Relation.Unary.Properties)
+  infixr  1 _⊎?_                                             (Relation.Unary.Properties)
+  infixr  7 _∩?_                                             (Relation.Unary.Properties)
+  infixr  6 _∪?_                                             (Relation.Unary.Properties)
+  infixl  6 _`⊜_                                             (Tactic.RingSolver)
+  infix   8 ⊝_                                               (Tactic.RingSolver.Core.Expression)
+  infix   4 _∈ᴿ?_ _∉ᴿ?_ _∈?ε _∈?[_] _∈?[^_]                  (Text.Regex.Properties)
+  infix   4 _∈?_ _∉?_                                        (Text.Regex.Derivative.Brzozowski)
+  infix   4 _∈_ _∉_ _∈?_ _∉?_                                (Text.Regex.String.Unsafe)
   ```
 
 * In `System.Exit`, the `ExitFailure` constructor is now carrying an integer

README/Design/Fixity.agda

@@ -23,6 +23,8 @@ module README.Design.Fixity where
 -- ternary reasoning infix 1 _⊢_≈_
 -- composition infixr 9 _∘_
 -- application infixr -1 _$_ _$!_
+-- combinatorics infixl 6.5 _P_ _P′_ _C_ _C′_
+-- pair infixr 4 _,_
 
 -- Reasoning:
 -- QED  infix  3 _∎

src/Data/Container/Relation/Binary/Pointwise.agda

@@ -26,6 +26,7 @@ module _ {s p} (C : Container s p) where
     constructor _,_
     field shape    : proj₁ cx ≡ proj₁ cy
           position : ∀ p → R (proj₂ cx p) (proj₂ cy (subst _ shape p))
+  infixr 4 _,_
 
 module _ {s p} {C : Container s p} {x y} {X : Set x} {Y : Set y}
          {ℓ ℓ′} {R : REL X Y ℓ} {R′ : REL X Y ℓ′}

src/Data/Nat/Combinatorics.agda

@@ -75,7 +75,7 @@ nCk≡nC[n∸k] {k} {n} k≤n = begin-equality
     _ = k !* (n ∸ k) !≢0
     _ = (n ∸ k) !* (n ∸ (n ∸ k)) !≢0
 
-nCk≡nPk/k! : k ≤ n → n C k ≡ (n P k / k !) {{k !≢0}}
+nCk≡nPk/k! : k ≤ n → n C k ≡ ((n P k) / k !) {{k !≢0}}
 nCk≡nPk/k! {k} {n} k≤n = begin-equality
   n C k                   ≡⟨ nCk≡n!/k![n-k]! k≤n ⟩
   n ! / (k ! * (n ∸ k) !) ≡˘⟨ /-congʳ (*-comm ((n ∸ k)!) (k !)) ⟩

src/Data/Nat/Combinatorics/Base.agda

@@ -25,6 +25,8 @@ open import Data.Nat.Properties using (_!≢0)
 
 -- n P k = n ! / (n ∸ k) !
 
+infixl 6.5 _P′_ _P_
+
 -- Base definition. Only valid for k ≤ n.
 
 _P′_ : ℕ → ℕ → ℕ
@@ -44,6 +46,8 @@ n P k = if k ≤ᵇ n then n P′ k else 0
 
 -- n C k = n ! / (k ! * (n ∸ k) !)
 
+infixl 6.5 _C′_ _C_
+
 -- Base definition. Only valid for k ≤ n.
 
 _C′_ : ℕ → ℕ → ℕ

src/Data/Nat/Combinatorics/Specification.agda

@@ -57,20 +57,20 @@ nP′k≡n[n∸1P′k∸1] : ∀ n k → .{{NonZero n}} → .{{NonZero k}} →
 nP′k≡n[n∸1P′k∸1] n           (suc zero)            = refl
 nP′k≡n[n∸1P′k∸1] n@(suc n-1) k@(suc k-1@(suc k-2)) = begin-equality
   n P′ k                        ≡⟨⟩
-  (n ∸ k-1) * n P′ k-1          ≡⟨ cong ((n ∸ k-1) *_) (nP′k≡n[n∸1P′k∸1] n k-1) ⟩
-  (n ∸ k-1) * (n * n-1 P′ k-2)  ≡⟨ x∙yz≈y∙xz (n ∸ k-1) n (n-1 P′ k-2) ⟩
-  n * ((n ∸ k-1) * n-1 P′ k-2)  ≡⟨⟩
-  n * n-1 P′ k-1                ∎
+  (n ∸ k-1) * (n P′ k-1)        ≡⟨ cong ((n ∸ k-1) *_) (nP′k≡n[n∸1P′k∸1] n k-1) ⟩
+  (n ∸ k-1) * (n * (n-1 P′ k-2))  ≡⟨ x∙yz≈y∙xz (n ∸ k-1) n (n-1 P′ k-2) ⟩
+  n * ((n ∸ k-1) * (n-1 P′ k-2))  ≡⟨⟩
+  n * (n-1 P′ k-1)              ∎
   where open ≤-Reasoning; open *-CS
 
 P′-rec : ∀ {n k} → k ≤ n → .{{NonZero k}} →
         n P′ k ≡ k * (pred n P′ pred k) + pred n P′ k
 P′-rec n@{suc n-1} k@{suc k-1} k≤n = begin-equality
-  n P′ k                                      ≡⟨ nP′k≡n[n∸1P′k∸1] n k ⟩
-  n * n-1 P′ k-1                              ≡˘⟨ cong (_* n-1 P′ k-1) (m+[n∸m]≡n {k} {n} k≤n) ⟩
-  (k + (n ∸ k)) * n-1 P′ k-1                  ≡⟨ *-distribʳ-+ (n-1 P′ k-1) k (n ∸ k) ⟩
-  k * (n-1 P′ k-1) + (n-1 ∸ k-1) * n-1 P′ k-1 ≡⟨⟩
-  k * (n-1 P′ k-1) + n-1 P′ k                 ∎
+  n P′ k                                        ≡⟨ nP′k≡n[n∸1P′k∸1] n k ⟩
+  n * (n-1 P′ k-1)                              ≡˘⟨ cong (_* (n-1 P′ k-1)) (m+[n∸m]≡n {k} {n} k≤n) ⟩
+  (k + (n ∸ k)) * (n-1 P′ k-1)                  ≡⟨ *-distribʳ-+ (n-1 P′ k-1) k (n ∸ k) ⟩
+  k * (n-1 P′ k-1) + (n-1 ∸ k-1) * (n-1 P′ k-1) ≡⟨⟩
+  k * (n-1 P′ k-1) + (n-1 P′ k)                 ∎
   where open ≤-Reasoning
 
 nP′n≡n! : ∀ n → n P′ n ≡ n !

src/Data/Refinement.agda

@@ -23,6 +23,7 @@ record Refinement {a p} (A : Set a) (P : A → Set p) : Set (a ⊔ p) where
   constructor _,_
   field value : A
         proof : Irrelevant (P value)
+infixr 4 _,_
 open Refinement public
 
 -- The syntax declaration below is meant to mimick set comprehension.

src/Data/Tree/AVL/Value.agda

@@ -34,6 +34,7 @@ record K&_ {v} (V : Value v) : Set (a ⊔ v) where
   field
     key   : Key
     value : Value.family V key
+infixr 4 _,_
 open K&_ public
 
 module _ {v} {V : Value v} where

src/Effect/Monad/Partiality.agda

@@ -517,6 +517,8 @@ module _ {A B : Set s}
 
   -- Bind preserves all the relations.
 
+  infixl 1 _>>=-cong_
+
   _>>=-cong_ :
     ∀ {k} {x₁ x₂ : A ⊥} {f₁ f₂ : A → B ⊥} → let open M in
     Rel _∼A_ k x₁ x₂ →
@@ -578,6 +580,8 @@ module _ {A B : Set ℓ} {_∼_ : B → B → Set ℓ} where
 
   -- A variant of _>>=-cong_.
 
+  infixl 1 _≡->>=-cong_
+
   _≡->>=-cong_ :
     ∀ {k} {x₁ x₂ : A ⊥} {f₁ f₂ : A → B ⊥} → let open M in
     Rel _≡_ k x₁ x₂ →

src/Effect/Monad/Partiality/All.agda

@@ -44,6 +44,8 @@ data All {A : Set a} (P : A → Set p) : A ⊥ → Set (a ⊔ p) where
 
 -- Bind preserves All in the following way:
 
+infixl 1 _>>=-cong_
+
 _>>=-cong_ : ∀ {p q} {P : A → Set p} {Q : B → Set q}
                {x : A ⊥} {f : A → B ⊥} →
              All P x → (∀ {x} → P x → All Q (f x)) →
@@ -118,6 +120,8 @@ module Alternative {a p : Level} where
     _≳⟨_⟩P_     : ∀ x {y} (x≳y : x ≳ y) (p : AllP P y) → AllP P x
     _⟨_⟩P       : ∀ x (p : AllP P x) → AllP P x
 
+  infixl 1 _>>=-congP_
+
   private
 
     -- WHNFs.

src/Effect/Monad/Predicate.agda

@@ -29,7 +29,7 @@ private
 
 record RawPMonad {I : Set i} (M : Pt I (i ⊔ ℓ)) : Set (suc i ⊔ suc ℓ) where
 
-  infixl 1 _?>=_ _?>_ _>?>_
+  infixl 1 _?>=_ _?>_ _>?>_ _?>=′_
   infixr 1 _=<?_ _<?<_
 
   -- ``Demonic'' operations (the opponent chooses the state).

src/Foreign/Haskell/Pair.agda

@@ -24,6 +24,7 @@ record Pair (A : Set a) (B : Set b) : Set (a ⊔ b) where
   constructor _,_
   field  fst : A
          snd : B
+infixr 4 _,_
 open Pair public
 
 {-# FOREIGN GHC type AgdaPair l1 l2 a b = (a , b) #-}

src/Function/Construct/Composition.agda

@@ -234,6 +234,8 @@ _↔-∘_ = inverse
 
 -- Version v2.0
 
+infix 8 _∘-⟶_ _∘-↣_ _∘-↠_ _∘-⤖_ _∘-⇔_ _∘-↩_ _∘-↪_ _∘-↔_
+
 _∘-⟶_ = _⟶-∘_
 {-# WARNING_ON_USAGE _∘-⟶_
 "Warning: _∘-⟶_ was deprecated in v2.0.

src/Reflection/AST/DeBruijn.agda

@@ -128,5 +128,7 @@ module _ where
     actions : ℕ → Actions
     actions i = record defaultActions { onVar = fvVar i }
 
+  infix 4 _∈FV_
+
   _∈FV_ : ℕ → Term → Bool
   i ∈FV t = traverseTerm (actions i) (0 , []) t

src/Reflection/AST/Traversal.agda

@@ -31,6 +31,7 @@ record Cxt : Set where
   field
     len     : ℕ
     context : List (String × Arg Term)
+infixr 4 _,_
 
 private
   _∷cxt_ : String × Arg Term → Cxt → Cxt

src/Reflection/AnnotatedAST.agda

@@ -83,6 +83,7 @@ Argₐ Tyₐ = ⟪ Argₐ′ Tyₐ ⟫
 
 data Namedₐ′ (Tyₐ : Typeₐ ℓ u) : Typeₐ ℓ (⟨named⟩ u) where
   _,_ : ∀ {t} x → Tyₐ Ann t → Namedₐ′ Tyₐ Ann (x , t)
+infixr 4 _,_
 
 Namedₐ : Typeₐ ℓ u → Typeₐ ℓ (⟨named⟩ u)
 Namedₐ Tyₐ = ⟪ Namedₐ′ Tyₐ ⟫

src/Relation/Binary/Construct/Composition.agda

@@ -26,6 +26,8 @@ private
 ------------------------------------------------------------------------
 -- Definition
 
+infixr 9 _;_
+
 _;_ : {A : Set a} {B : Set b} {C : Set c} →
       REL A B ℓ₁ → REL B C ℓ₂ → REL A C (b ⊔ ℓ₁ ⊔ ℓ₂)
 L ; R = λ i j → ∃ λ k → L i k × R k j

src/Relation/Binary/HeterogeneousEquality/Quotients/Examples.agda

@@ -59,10 +59,12 @@ module Integers (quot : Quotients 0ℓ 0ℓ) where
 
   open Quotient Int renaming (Q to ℤ)
 
+  infixl 6 _+²_
+
   _+²_ : ℕ² → ℕ² → ℕ²
   (x₁ , y₁) +² (x₂ , y₂) = x₁ + x₂ , y₁ + y₂
 
-  +²-cong : ∀{a b a′ b′} → a ∼ a′ → b ∼ b′ → a +² b ∼ a′ +² b′
+  +²-cong : ∀{a b a′ b′} → a ∼ a′ → b ∼ b′ → (a +² b) ∼ (a′ +² b′)
   +²-cong {a₁ , b₁} {c₁ , d₁} {a₂ , b₂} {c₂ , d₂} ab∼cd₁ ab∼cd₂ = begin
     (a₁ + c₁) + (b₂ + d₂) ≡⟨ ≡.cong (_+ (b₂ + d₂)) (+-comm a₁ c₁) ⟩
     (c₁ + a₁) + (b₂ + d₂) ≡⟨ +-assoc c₁ a₁ (b₂ + d₂) ⟩
@@ -128,7 +130,7 @@ module Integers (quot : Quotients 0ℓ 0ℓ) where
         abs (zero² +² a)   ≅⟨ compat-abs (+²-identityˡ a) ⟩
         abs a              ∎
 
-    +²-assoc : (i j k : ℕ²) → (i +² j) +² k ∼ i +² (j +² k)
+    +²-assoc : (i j k : ℕ²) → ((i +² j) +² k) ∼ (i +² (j +² k))
     +²-assoc (a , b) (c , d) (e , f) = begin
       ((a + c) + e) + (b + (d + f)) ≡⟨ ≡.cong (_+ (b + (d + f))) (+-assoc a c e) ⟩
       (a + (c + e)) + (b + (d + f)) ≡⟨ ≡.cong ((a + (c + e)) +_) (≡.sym (+-assoc b d f)) ⟩

src/Relation/Binary/Indexed/Heterogeneous/Construct/At.agda

@@ -64,5 +64,7 @@ module _ {a i} {I : Set i} where
 
 module _ {a i} {I : Set i} where
 
+  infixr -1 _atₛ_
+
   _atₛ_ : ∀ {ℓ} → IndexedSetoid I a ℓ → I → Setoid a ℓ
   _atₛ_ = setoid

src/Relation/Binary/Indexed/Homogeneous/Construct/At.agda

@@ -68,5 +68,7 @@ preorder O index = record
 ------------------------------------------------------------------------
 -- Some useful shorthand infix notation
 
+infixr -1 _atₛ_
+
 _atₛ_ : ∀ {ℓ} → IndexedSetoid I a ℓ → I → Setoid a ℓ
 _atₛ_ = setoid

src/Relation/Unary/Indexed.agda

@@ -17,6 +17,8 @@ IPred A ℓ = ∀ {i} → A i → Set ℓ
 
 module _ {i a} {I : Set i} {A : I → Set a} where
 
+  infix 4 _∈_ _∉_
+
   _∈_ : ∀ {ℓ} → (∀ i → A i) → IPred A ℓ → Set _
   x ∈ P = ∀ i → P (x i)
 

src/Relation/Unary/PredicateTransformer.agda

@@ -34,6 +34,8 @@ Pt A ℓ = PT A A ℓ ℓ
 ------------------------------------------------------------------------
 -- Composition and identity
 
+infixr 9 _⍮_
+
 _⍮_ : PT B C ℓ₂ ℓ₃ → PT A B ℓ₁ ℓ₂ → PT A C ℓ₁ _
 S ⍮ T = S ∘ T
 
@@ -53,6 +55,8 @@ magic = λ _ → U
 
 -- Negation.
 
+infix 8 ∼_
+
 ∼_ : PT A B ℓ₁ ℓ₂ → PT A B ℓ₁ ℓ₂
 ∼ T = ∁ ∘ T
 

src/Relation/Unary/Properties.agda

@@ -202,6 +202,12 @@ U-Universal = λ _ → _
 ∁? : {P : Pred A ℓ} → Decidable P → Decidable (∁ P)
 ∁? P? x = ¬? (P? x)
 
+infix 2 _×?_ _⊙?_
+infix 10 _~?
+infixr 1 _⊎?_
+infixr 7 _∩?_
+infixr 6 _∪?_
+
 _∪?_ : {P : Pred A ℓ₁} {Q : Pred A ℓ₂} →
        Decidable P → Decidable Q → Decidable (P ∪ Q)
 _∪?_ P? Q? x = (P? x) ⊎-dec (Q? x)

src/Tactic/RingSolver.agda

@@ -141,6 +141,8 @@ module RingSolverReflection (ring : Term) (numberOfVariables : ℕ) where
   `I : Term → Term
   `I x = quote Ι $ᵉ (x ⟨∷⟩ [])
 
+  infixl 6 _`⊜_
+
   _`⊜_ : Term → Term → Term
   x `⊜ y = quote _⊜_  $ʳ (`numberOfVariables ⟅∷⟆ x ⟨∷⟩ y ⟨∷⟩ [])
 

src/Tactic/RingSolver/Core/Expression.agda

@@ -17,6 +17,7 @@ open import Algebra
 infixl 6 _⊕_
 infixl 7 _⊗_
 infixr 8 _⊛_
+infix 8 ⊝_
 
 data Expr {a} (A : Set a) (n : ℕ) : Set a where
   Κ   : A → Expr A n                   -- Constant

src/Text/Regex/Derivative/Brzozowski.agda

@@ -107,6 +107,8 @@ eat-complete′ x (e R.⋆) (refl ∷ eq) (star (sum (inj₂ (prod (refl ∷ app
 ------------------------------------------------------------------------
 -- Consequence: matching is decidable
 
+infix 4 _∈?_ _∉?_
+
 _∈?_ : Decidable _∈_
 []       ∈? e = []∈? e
 (x ∷ xs) ∈? e = map′ (eat-sound x e) (eat-complete x e) (xs ∈? eat x e)

src/Text/Regex/Properties.agda

@@ -49,6 +49,8 @@ open import Text.Regex.Properties.Core preorder public
              $ ([]∈? e) ×-dec ([]∈? f)
 []∈? (e ⋆)   = yes (star (sum (inj₁ ε)))
 
+infix 4 _∈ᴿ?_ _∉ᴿ?_ _∈?ε _∈?[_] _∈?[^_]
+
 _∈ᴿ?_ : Decidable _∈ᴿ_
 c ∈ᴿ? [ a ]     = map′ [_] (λ where [ eq ] → eq) (c ≟ a)
 c ∈ᴿ? (lb ─ ub) = map′ (uncurry _─_) (λ where (ge ─ le) → ge , le)

src/Text/Regex/String/Unsafe.agda

@@ -26,6 +26,8 @@ open import Text.Regex.String as Regex public
 ------------------------------------------------------------------------
 -- Specialised definitions
 
+infix 4 _∈_ _∉_ _∈?_ _∉?_
+
 _∈_ : String → Exp → Set
 str ∈ e = toList str Regex.∈ e