Add more fixities (#2008)

Author: Saransh-cpp

CHANGELOG.md

@@ -112,6 +112,14 @@ Bug-fixes
   infix   4 _≈∙_                                             (Relation.Binary.Construct.Add.Point.Equality)
   infix   4 _≤⁺_ _≤⊤⁺                                        (Relation.Binary.Construct.Add.Supremum.NonStrict)
   infixr  5 _∷ʳ_                                             (Relation.Binary.Construct.Closure.Transitive)
+  infixr  5 _∷_                                              (Codata.Guarded.Stream.Relation.Unary.All)
+  infixr  5 _∷_                                              (Foreign.Haskell.List.NonEmpty)
+  infix   4 _≈_                                              (Function.Metric.Rational.Bundles)
+  infixl  6 _ℕ+_                                             (Level.Literals)
+  infixr  6 _∪_                                              (Relation.Binary.Construct.Union)
+  infixl  6 _+ℤ_                                             (Relation.Binary.HeterogeneousEquality.Quotients.Examples)
+  infix   4 _≉_ _≈ᵢ_ _≤ᵢ_                                    (Relation.Binary.Indexed.Homogeneous.Bundles)
+  infixr  5 _∷ᴹ_ _∷⁻¹ᴹ_                                      (Text.Regex.Search)
   ```
 
 * In `System.Exit`, the `ExitFailure` constructor is now carrying an integer

src/Codata/Guarded/Stream/Relation/Unary/All.agda

@@ -20,6 +20,8 @@ private
     P Q R : Pred A p
     xs : Stream A
 
+infixr 5 _∷_
+
 record All (P : Pred A ℓ) (as : Stream A) : Set ℓ where
   coinductive
   constructor _∷_

src/Foreign/Haskell/List/NonEmpty.agda

@@ -25,5 +25,7 @@ private
 data NonEmpty (A : Set a) : Set a where
   _∷_ : A → List A → NonEmpty A
 
+infixr 5 _∷_
+
 {-# FOREIGN GHC type AgdaNonEmpty l a = NE.NonEmpty a #-}
 {-# COMPILE GHC NonEmpty = data AgdaNonEmpty ((NE.:|)) #-}

src/Function/Metric/Rational/Bundles.agda

@@ -34,6 +34,8 @@ record ProtoMetric a ℓ : Set (suc (a ⊔ ℓ)) where
     d             : DistanceFunction Carrier
     isProtoMetric : IsProtoMetric _≈_ d
 
+  infix 4 _≈_
+
   open IsProtoMetric isProtoMetric public
 
 ------------------------------------------------------------------------
@@ -46,6 +48,8 @@ record PreMetric a ℓ : Set (suc (a ⊔ ℓ)) where
     d           : DistanceFunction Carrier
     isPreMetric : IsPreMetric _≈_ d
 
+  infix 4 _≈_
+
   open IsPreMetric isPreMetric public
 
   protoMetric : ProtoMetric a ℓ
@@ -63,6 +67,8 @@ record QuasiSemiMetric a ℓ : Set (suc (a ⊔ ℓ)) where
     d                 : DistanceFunction Carrier
     isQuasiSemiMetric : IsQuasiSemiMetric _≈_ d
 
+  infix 4 _≈_
+
   open IsQuasiSemiMetric isQuasiSemiMetric public
 
   preMetric : PreMetric a ℓ
@@ -83,6 +89,8 @@ record SemiMetric a ℓ : Set (suc (a ⊔ ℓ)) where
     d            : DistanceFunction Carrier
     isSemiMetric : IsSemiMetric _≈_ d
 
+  infix 4 _≈_
+
   open IsSemiMetric isSemiMetric public
 
   quasiSemiMetric : QuasiSemiMetric a ℓ
@@ -103,6 +111,8 @@ record Metric a ℓ : Set (suc (a ⊔ ℓ)) where
     d        : DistanceFunction Carrier
     isMetric : IsMetric _≈_ d
 
+  infix 4 _≈_
+
   open IsMetric isMetric public
 
   semiMetric : SemiMetric a ℓ
@@ -123,6 +133,8 @@ record UltraMetric a ℓ : Set (suc (a ⊔ ℓ)) where
     d             : DistanceFunction Carrier
     isUltraMetric : IsUltraMetric _≈_ d
 
+  infix 4 _≈_
+
   open IsUltraMetric isUltraMetric public
 
   semiMetric : SemiMetric a ℓ

src/Level/Literals.agda

@@ -15,6 +15,8 @@ open import Level using (Level; 0ℓ)
 
 -- Increase a Level by a number of sucs.
 
+infixl 6 _ℕ+_
+
 _ℕ+_ : ℕ → Level → Level
 zero  ℕ+ ℓ = ℓ
 suc n ℕ+ ℓ = Level.suc (n ℕ+ ℓ)

src/Relation/Binary/Construct/Union.agda

@@ -24,6 +24,8 @@ private
 ------------------------------------------------------------------------
 -- Definition
 
+infixr 6 _∪_
+
 _∪_ : REL A B ℓ₁ → REL A B ℓ₂ → REL A B (ℓ₁ ⊔ ℓ₂)
 L ∪ R = λ i j → L i j ⊎ R i j
 

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

@@ -82,6 +82,8 @@ module Integers (quot : Quotients 0ℓ 0ℓ) where
   module _ (ext : ∀ {a b} {A : Set a} {B₁ B₂ : A → Set b} {f₁ : ∀ a → B₁ a}
                   {f₂ : ∀ a → B₂ a} → (∀ a → f₁ a ≅ f₂ a) → f₁ ≅ f₂) where
 
+    infixl 6 _+ℤ_
+
     _+ℤ_ : ℤ → ℤ → ℤ
     _+ℤ_ = Properties₂.lift₂ ext Int Int (λ i j → abs (i +² j))
          $ λ {a} {b} {c} p p′ → compat-abs (+²-cong {a} {b} {c} p p′)

src/Relation/Binary/Indexed/Homogeneous/Bundles.agda

@@ -39,6 +39,8 @@ record IndexedSetoid {i} (I : Set i) c ℓ : Set (suc (i ⊔ c ⊔ ℓ)) where
   Carrier : Set _
   Carrier = ∀ i → Carrierᵢ i
 
+  infix 4 _≉_
+
   _≈_ : B.Rel Carrier _
   _≈_ = Lift Carrierᵢ _≈ᵢ_
 
@@ -103,6 +105,7 @@ record IndexedPreorder {i} (I : Set i) c ℓ₁ ℓ₂ :
 
 record IndexedPoset {i} (I : Set i) c ℓ₁ ℓ₂ :
                     Set (suc (i ⊔ c ⊔ ℓ₁ ⊔ ℓ₂)) where
+  infix 4 _≈ᵢ_ _≤ᵢ_
   field
     Carrierᵢ        : I → Set c
     _≈ᵢ_            : IRel Carrierᵢ ℓ₁

src/Text/Regex/Search.agda

@@ -87,6 +87,8 @@ module Prefix where
   []⁻¹ᴹ : ∀ {e} → Match (Prefix _≡_) [] e → [] ∈ e
   []⁻¹ᴹ (mkMatch .[] p []) = p
 
+  infixr 5 _∷ᴹ_ _∷⁻¹ᴹ_
+
   _∷ᴹ_ : ∀ {xs e} x → Match (Prefix _≡_) xs (eat x e) → Match (Prefix _≡_) (x ∷ xs) e
   x ∷ᴹ (mkMatch ys ys∈e\x ys≤xs) = mkMatch (x ∷ ys) (eat-sound x _ ys∈e\x) (refl ∷ ys≤xs)