Fixities for Relation and Algebra (#1992)

Author: Saransh-cpp

CHANGELOG.md

@@ -105,6 +105,13 @@ Bug-fixes
   infix   8 _⁻¹                                              (Data.Parity.Base)
   infixr  5 _`∷_                                             (Data.Vec.Reflection)
   infixr  5 _∷=_                                             (Data.Vec.Membership.Setoid)
+  infix   4 _≟H_ _≟N_                                        (Algebra.Solver.Ring)
+  infix   4 _≈_                                              (Relation.Binary.Bundles)
+  infixl  6 _∩_                                              (Relation.Binary.Construct.Intersection)
+  infix   4 _<₋_                                             (Relation.Binary.Construct.Add.Infimum.Strict)
+  infix   4 _≈∙_                                             (Relation.Binary.Construct.Add.Point.Equality)
+  infix   4 _≤⁺_ _≤⊤⁺                                        (Relation.Binary.Construct.Add.Supremum.NonStrict)
+  infixr  5 _∷ʳ_                                             (Relation.Binary.Construct.Closure.Transitive)
   ```
 
 * In `System.Exit`, the `ExitFailure` constructor is now carrying an integer

src/Algebra/Solver/Ring.agda

@@ -176,6 +176,8 @@ mutual
 
   -- Equality is weakly decidable.
 
+  infix 4 _≟H_ _≟N_
+
   _≟H_ : ∀ {n} → WeaklyDecidable (_≈H_ {n = n})
   ∅           ≟H ∅           = just ∅
   ∅           ≟H (_ *x+ _)   = nothing

src/Relation/Binary/Bundles.agda

@@ -21,6 +21,7 @@ open import Relation.Binary.Structures
 ------------------------------------------------------------------------
 
 record PartialSetoid a ℓ : Set (suc (a ⊔ ℓ)) where
+  infix 4 _≈_
   field
     Carrier              : Set a
     _≈_                  : Rel Carrier ℓ

src/Relation/Binary/Construct/Add/Infimum/Strict.agda

@@ -28,6 +28,8 @@ import Relation.Nullary.Decidable as Dec
 ------------------------------------------------------------------------
 -- Definition
 
+infix 4 _<₋_
+
 data _<₋_ : Rel (A ₋) (a ⊔ ℓ) where
   ⊥₋<[_] : (l : A)           → ⊥₋    <₋ [ l ]
   [_]    : {k l : A} → k < l → [ k ] <₋ [ l ]

src/Relation/Binary/Construct/Add/Point/Equality.agda

@@ -24,6 +24,8 @@ import Relation.Nullary.Decidable as Dec
 ------------------------------------------------------------------------
 -- Definition
 
+infix 4 _≈∙_
+
 data _≈∙_ : Rel (Pointed A) (a ⊔ ℓ) where
   ∙≈∙ :                     ∙     ≈∙ ∙
   [_] : {k l : A} → k ≈ l → [ k ] ≈∙ [ l ]

src/Relation/Binary/Construct/Add/Supremum/NonStrict.agda

@@ -26,6 +26,8 @@ import Relation.Binary.Construct.Add.Supremum.Equality as Equality
 ------------------------------------------------------------------------
 -- Definition
 
+infix 4 _≤⁺_ _≤⊤⁺
+
 data _≤⁺_ : Rel (A ⁺) (a ⊔ ℓ) where
   [_]  : {k l : A} → k ≤ l → [ k ] ≤⁺ [ l ]
   _≤⊤⁺ : (k : A ⁺)         → k     ≤⁺ ⊤⁺

src/Relation/Binary/Construct/Closure/Transitive.agda

@@ -39,6 +39,8 @@ module _ {_∼_ : Rel A ℓ} where
   private
     _∼⁺_ = TransClosure _∼_
 
+  infixr 5 _∷ʳ_
+
   _∷ʳ_ : ∀ {x y z} → (x∼⁺y : x ∼⁺ y) (y∼z : y ∼ z) → x ∼⁺ z
   [ x∼y ]      ∷ʳ y∼z = x∼y ∷ [ y∼z ]
   (x∼y ∷ x∼⁺y) ∷ʳ y∼z = x∼y ∷ (x∼⁺y ∷ʳ y∼z)

src/Relation/Binary/Construct/Intersection.agda

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