Fixities for Data and Codata (#1985)

Saransh-cpp · web-flow · commit a5b35647ed64 · 2023-06-19T10:25:51.000+09:00
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -29,6 +29,35 @@ Highlights
 Bug-fixes
 ---------
 
+* The following operators were missing a fixity declaration, which has now
+  been fixed -
+  ```
+  infix  4 _ℕ<_ _ℕ≤infinity _ℕ≤_                            (Codata.Sized.Conat)
+  infix  6 _ℕ+_ _+ℕ_                                        (Codata.Sized.Conat)
+  infixl 4 _+ _*                                            (Data.List.Kleene.Base)
+  infixr 4 _++++_ _+++*_ _*+++_ _*++*_                      (Data.List.Kleene.Base)
+  infix  4 _[_]* _[_]+                                      (Data.List.Kleene.Base)
+  infix  4 _≢∈_                                             (Data.List.Membership.Propositional)
+  infixr 5 _`∷_                                             (Data.List.Reflection)
+  infix  4 _≡?_                                             (Data.List.Relation.Binary.Equality.DecPropositional)
+  infixr 5 _++ᵖ_                                            (Data.List.Relation.Binary.Prefix.Heterogeneous)
+  infixr 5 _++ˢ_                                            (Data.List.Relation.Binary.Suffix.Heterogeneous)
+  infixr 5 _++_ _++[]                                       (Data.List.Relation.Ternary.Appending.Propositional)
+  infixr 5 _∷=_                                             (Data.List.Relation.Unary.Any)
+  infixr 5 _++_                                             (Data.List.Ternary.Appending)
+  infixr 2 _×-⇔_ _×-↣_ _×-↞_ _×-↠_ _×-↔_ _×-cong_           (Data.Product.Function.NonDependent.Propositional)
+  infixr 2 _×-⟶_                                           (Data.Product.Function.NonDependent.Setoid)
+  infixr 2 _×-equivalence_ _×-injection_ _×-left-inverse_   (Data.Product.Function.NonDependent.Setoid)
+  infixr 2 _×-surjection_ _×-inverse_                       (Data.Product.Function.NonDependent.Setoid)
+  infixr 1 _⊎-⇔_ _⊎-↣_ _⊎-↞_ _⊎-↠_ _⊎-↔_ _⊎-cong_           (Data.Sum.Function.Propositional)
+  infixr 1 _⊎-⟶_                                           (Data.Sum.Function.Setoid)
+  infixr 1 _⊎-equivalence_ _⊎-injection_ _⊎-left-inverse_   (Data.Sum.Function.Setoid)
+  infixr 1 _⊎-surjection_ _⊎-inverse_                       (Data.Sum.Function.Setoid)
+  infix  8 _⁻¹                                              (Data.Parity.Base)
+  infixr 5 _`∷_                                             (Data.Vec.Reflection)
+  infixr 5 _∷=_                                             (Data.Vec.Membership.Setoid)
+  ```
+
 * In `System.Exit`, the `ExitFailure` constructor is now carrying an integer
   rather than a natural. The previous binding was incorrectly assuming that
   all exit codes where non-negative.
diff --git a/src/Algebra/Definitions.agda b/src/Algebra/Definitions.agda
@@ -109,7 +109,7 @@ _DistributesOver_ : Op₂ A → Op₂ A → Set _
 * DistributesOver + = (* DistributesOverˡ +) × (* DistributesOverʳ +)
 
 _MiddleFourExchange_ : Op₂ A → Op₂ A → Set _
-_*_ MiddleFourExchange _+_ = 
+_*_ MiddleFourExchange _+_ =
   ∀ w x y z → ((w + x) * (y + z)) ≈ ((w + y) * (x + z))
 
 _IdempotentOn_ : Op₂ A → A → Set _
diff --git a/src/Codata/Sized/Conat.agda b/src/Codata/Sized/Conat.agda
@@ -35,7 +35,7 @@ pred : ∀ {i} {j : Size< i} → Conat i → Conat j
 pred zero    = zero
 pred (suc n) = n .force
 
-infixl 6 _∸_ _+_
+infixl 6 _∸_ _+_ _ℕ+_ _+ℕ_
 infixl 7 _*_
 
 _∸_ : Conat ∞ → ℕ → Conat ∞
@@ -91,6 +91,8 @@ toℕ (suc n) = suc (toℕ n)
 ------------------------------------------------------------------------
 -- Order wrt to Nat
 
+infix 4 _ℕ<_ _ℕ≤infinity _ℕ≤_
+
 data _ℕ≤_ : ℕ → Conat ∞ → Set where
   zℕ≤n : ∀ {n} → zero ℕ≤ n
   sℕ≤s : ∀ {k n} → k ℕ≤ n .force → suc k ℕ≤ suc n
diff --git a/src/Data/List/Kleene/Base.agda b/src/Data/List/Kleene/Base.agda
@@ -40,6 +40,7 @@ private
 --   simplify certain proofs.
 
 infixr 5 _&_ ∹_
+infixl 4 _+ _*
 
 record _+ {a} (A : Set a) : Set a
 data _* {a} (A : Set a) : Set a
@@ -101,6 +102,7 @@ module _ (f : B → A → B) where
 -- Concatenation
 
 module Concat where
+  infixr 4 _++++_ _+++*_ _*+++_ _*++*_
   _++++_ : A + → A + → A +
   _+++*_ : A + → A * → A +
   _*+++_ : A * → A + → A +
@@ -270,6 +272,8 @@ module _ (f : A → Maybe B → B) where
 ------------------------------------------------------------------------
 -- Indexing
 
+infix 4 _[_]* _[_]+
+
 _[_]* : A * → ℕ → Maybe A
 _[_]+ : A + → ℕ → Maybe A
 
diff --git a/src/Data/List/Membership/Propositional.agda b/src/Data/List/Membership/Propositional.agda
@@ -22,6 +22,8 @@ open SetoidMembership (setoid A) public hiding (lose)
 ------------------------------------------------------------------------
 -- Different members
 
+infix 4 _≢∈_
+
 _≢∈_ : ∀ {x y : A} {xs} → x ∈ xs → y ∈ xs → Set _
 _≢∈_ x∈xs y∈xs = ∀ x≡y → subst (_∈ _) x≡y x∈xs ≢ y∈xs
 
diff --git a/src/Data/List/Reflection.agda b/src/Data/List/Reflection.agda
@@ -24,6 +24,8 @@ open import Reflection.AST.Argument
 `[] : Term
 `[] = con (quote List.[]) (2 ⋯⟅∷⟆ [])
 
+infixr 5 _`∷_
+
 _`∷_ : Term → Term → Term
 x `∷ xs = con (quote List._∷_) (2 ⋯⟅∷⟆ x ⟨∷⟩ xs ⟨∷⟩ [])
 
diff --git a/src/Data/List/Relation/Binary/Equality/DecPropositional.agda b/src/Data/List/Relation/Binary/Equality/DecPropositional.agda
@@ -32,5 +32,7 @@ open DecSetoidEq (decSetoid _≟_) public
 ------------------------------------------------------------------------
 -- Additional proofs
 
+infix 4 _≡?_
+
 _≡?_ : Decidable (_≡_ {A = List A})
 _≡?_ = ≡-dec _≟_
diff --git a/src/Data/List/Relation/Binary/Prefix/Heterogeneous.agda b/src/Data/List/Relation/Binary/Prefix/Heterogeneous.agda
@@ -45,6 +45,8 @@ module _ {a b r s} {A : Set a} {B : Set b} {R : REL A B r} {S : REL A B s} where
 
 module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
 
+  infixr 5 _++ᵖ_
+
   _++ᵖ_ : ∀ {as bs} → Prefix R as bs → ∀ suf → Prefix R as (bs List.++ suf)
   []       ++ᵖ suf = []
   (r ∷ rs) ++ᵖ suf = r ∷ (rs ++ᵖ suf)
diff --git a/src/Data/List/Relation/Binary/Suffix/Heterogeneous.agda b/src/Data/List/Relation/Binary/Suffix/Heterogeneous.agda
@@ -31,6 +31,8 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
   tail (here (_ ∷ rs)) = there (here rs)
   tail (there x) = there (tail x)
 
+  infixr 5 _++ˢ_
+
   _++ˢ_ : ∀ pre {as bs} → Suffix R as bs → Suffix R as (pre List.++ bs)
   []       ++ˢ rs = rs
   (x ∷ xs) ++ˢ rs = there (xs ++ˢ rs)
diff --git a/src/Data/List/Relation/Ternary/Appending.agda b/src/Data/List/Relation/Ternary/Appending.agda
@@ -38,6 +38,8 @@ module _ (L : REL A C l) (R : REL B C r) where
 ------------------------------------------------------------------------
 -- Functions manipulating Appending
 
+infixr 5 _++_
+
 _++_ : ∀ {cs₁ cs₂ : List C} → Pointwise L as cs₁ → Pointwise R bs cs₂ →
        Appending L R as bs (cs₁ List.++ cs₂)
 []       ++ rs = []++ rs
diff --git a/src/Data/List/Relation/Ternary/Appending/Propositional.agda b/src/Data/List/Relation/Ternary/Appending/Propositional.agda
@@ -32,6 +32,8 @@ open General public
 ------------------------------------------------------------------------
 -- Definition
 
+infixr 5 _++_ _++[]
+
 _++_ : (as bs : List A) → Appending as bs (as List.++ bs)
 as ++ bs = Pw.≡⇒Pointwise-≡ refl General.++ Pw.≡⇒Pointwise-≡ refl
 
diff --git a/src/Data/List/Relation/Unary/Any.agda b/src/Data/List/Relation/Unary/Any.agda
@@ -62,6 +62,8 @@ index (there pxs) = suc (index pxs)
 lookup : {P : Pred A p} → Any P xs → A
 lookup {xs = xs} p = List.lookup xs (index p)
 
+infixr 5 _∷=_
+
 _∷=_ : {P : Pred A p} → Any P xs → A → List A
 _∷=_ {xs = xs} x∈xs v = xs List.[ index x∈xs ]∷= v
 
diff --git a/src/Data/Parity/Base.agda b/src/Data/Parity/Base.agda
@@ -26,6 +26,8 @@ data Parity : Set where
 
 -- The opposite parity.
 
+infix 8 _⁻¹
+
 _⁻¹ : Parity → Parity
 1ℙ ⁻¹ = 0ℙ
 0ℙ ⁻¹ = 1ℙ
diff --git a/src/Data/Product/Function/NonDependent/Propositional.agda b/src/Data/Product/Function/NonDependent/Propositional.agda
@@ -27,6 +27,8 @@ open import Function.Surjection as Surj using (_↠_; module Surjection)
 
 module _ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} where
 
+  infixr 2 _×-⇔_ _×-↣_ _×-↞_ _×-↠_ _×-↔_
+
   _×-⇔_ : A ⇔ B → C ⇔ D → (A × C) ⇔ (B × D)
   _×-⇔_ A⇔B C⇔D =
     Inverse.equivalence Pointwise-≡↔≡           ⟨∘⟩
@@ -64,6 +66,8 @@ module _ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} where
 
 module _ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} where
 
+  infixr 2 _×-cong_
+
   _×-cong_ : ∀ {k} → A ∼[ k ] B → C ∼[ k ] D → (A × C) ∼[ k ] (B × D)
   _×-cong_ {implication}         = λ f g →      map        f         g
   _×-cong_ {reverse-implication} = λ f g → lam (map (app-← f) (app-← g))
diff --git a/src/Data/Product/Function/NonDependent/Setoid.agda b/src/Data/Product/Function/NonDependent/Setoid.agda
@@ -33,6 +33,8 @@ module _  {a₁ a₂ b₁ b₂ c₁ c₂ d₁ d₂}
           {C : Setoid c₁ c₂} {D : Setoid d₁ d₂}
           where
 
+  infixr 2 _×-⟶_
+
   _×-⟶_ : (A ⟶ B) → (C ⟶ D) → (A ×ₛ C) ⟶ (B ×ₛ D)
   _×-⟶_ f g = record
     { _⟨$⟩_ = fg
@@ -76,6 +78,8 @@ module _  {a₁ a₂ b₁ b₂ c₁ c₂ d₁ d₂}
           {C : Setoid c₁ c₂} {D : Setoid d₁ d₂}
           where
 
+  infixr 2 _×-equivalence_ _×-injection_ _×-left-inverse_
+
   _×-equivalence_ : Equivalence A B → Equivalence C D →
                     Equivalence (A ×ₛ C) (B ×ₛ D)
   _×-equivalence_ A⇔B C⇔D = record
@@ -110,6 +114,8 @@ module _ {a₁ a₂ b₁ b₂ c₁ c₂ d₁ d₂}
   {C : Setoid c₁ c₂} {D : Setoid d₁ d₂}
   where
 
+  infixr 2 _×-surjection_ _×-inverse_
+
   _×-surjection_ : Surjection A B → Surjection C D →
                    Surjection (A ×ₛ C) (B ×ₛ D)
   A↠B ×-surjection C↠D = record
diff --git a/src/Data/Sum/Function/Propositional.agda b/src/Data/Sum/Function/Propositional.agda
@@ -24,6 +24,8 @@ open import Function.Surjection as Surj using (_↠_; module Surjection)
 
 module _ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} where
 
+  infixr 1 _⊎-⇔_ _⊎-↣_ _⊎-↞_ _⊎-↠_ _⊎-↔_
+
   _⊎-⇔_ : A ⇔ B → C ⇔ D → (A ⊎ C) ⇔ (B ⊎ D)
   _⊎-⇔_ A⇔B C⇔D =
     Inverse.equivalence (Pointwise-≡↔≡ B D) ⟨∘⟩
@@ -61,6 +63,8 @@ module _ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} where
 
 module _ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} where
 
+  infixr 1 _⊎-cong_
+
   _⊎-cong_ : ∀ {k} → A ∼[ k ] B → C ∼[ k ] D → (A ⊎ C) ∼[ k ] (B ⊎ D)
   _⊎-cong_ {implication}         = map
   _⊎-cong_ {reverse-implication} = λ f g → lam (map (app-← f) (app-← g))
diff --git a/src/Data/Sum/Function/Setoid.agda b/src/Data/Sum/Function/Setoid.agda
@@ -32,6 +32,8 @@ module _  {a₁ a₂ b₁ b₂ c₁ c₂ d₁ d₂}
           {C : Setoid c₁ c₂} {D : Setoid d₁ d₂}
           where
 
+  infixr 1 _⊎-⟶_
+
   _⊎-⟶_ : (A ⟶ B) → (C ⟶ D) → (A ⊎ₛ C) ⟶ (B ⊎ₛ D)
   _⊎-⟶_ f g = record
     { _⟨$⟩_ = fg
@@ -77,6 +79,8 @@ module _  {a₁ a₂ b₁ b₂ c₁ c₂ d₁ d₂}
           {C : Setoid c₁ c₂} {D : Setoid d₁ d₂}
           where
 
+  infixr 1 _⊎-equivalence_ _⊎-injection_ _⊎-left-inverse_
+
   _⊎-equivalence_ : Equivalence A B → Equivalence C D →
                     Equivalence (A ⊎ₛ C) (B ⊎ₛ D)
   A⇔B ⊎-equivalence C⇔D = record
@@ -119,6 +123,7 @@ module _ {a₁ a₂ b₁ b₂ c₁ c₂ d₁ d₂}
          {C : Setoid c₁ c₂} {D : Setoid d₁ d₂}
          where
 
+  infixr 1 _⊎-surjection_ _⊎-inverse_
   _⊎-surjection_ : Surjection A B → Surjection C D →
                    Surjection (A ⊎ₛ C) (B ⊎ₛ D)
   A↠B ⊎-surjection C↠D = record
diff --git a/src/Data/Vec/Membership/Setoid.agda b/src/Data/Vec/Membership/Setoid.agda
@@ -39,6 +39,8 @@ mapWith∈ : ∀ {b} {B : Set b} {n}
 mapWith∈ []       f = []
 mapWith∈ (x ∷ xs) f = f (here refl) ∷ mapWith∈ xs (f ∘ there)
 
+infixr 5 _∷=_
+
 _∷=_ : ∀ {n} {xs : Vec A n} {x} → x ∈ xs → A → Vec A n
 _∷=_ {xs = xs} x∈xs v = xs Vec.[ index x∈xs ]≔ v
 
diff --git a/src/Data/Vec/Reflection.agda b/src/Data/Vec/Reflection.agda
@@ -25,6 +25,8 @@ open import Reflection.AST.Argument
 `[] : Term
 `[] = con (quote []) (2 ⋯⟅∷⟆ List.[])
 
+infixr 5 _`∷_
+
 _`∷_ : Term → Term → Term
 _`∷_ x xs = con (quote _∷_) (3 ⋯⟅∷⟆ x ⟨∷⟩ xs ⟨∷⟩ List.[])
 
