Fixities for Function, Data, and Reflection (#1987)

Author: Saransh-cpp

CHANGELOG.md

@@ -31,7 +31,27 @@ Bug-fixes
 
 * The following operators were missing a fixity declaration, which has now
   been fixed -
-  ```
+   ```
+  infix  -1 _$ⁿ_          (Data.Vec.N-ary)
+  infix  4 _≋_            (Data.Vec.Functional.Relation.Binary.Equality.Setoid)
+  infix  4 _≟_            (Reflection.AST.Definition)
+  infix  4 _≡ᵇ_           (Reflection.AST.Literal)
+  infix  4 _≈?_ _≟_ _≈_   (Reflection.AST.Meta)
+  infix  4 _≈?_ _≟_ _≈_   (Reflection.AST.Name)
+  infix  4 _≟-Telescope_  (Reflection.AST.Term)
+  infix  4 _≟_            (Reflection.AST.Argument.Information)
+  infix  4 _≟_            (Reflection.AST.Argument.Modality)
+  infix  4 _≟_            (Reflection.AST.Argument.Quantity)
+  infix  4 _≟_            (Reflection.AST.Argument.Relevance)
+  infix  4 _≟_            (Reflection.AST.Argument.Visibility)
+  infixr 8 _^_            (Function.Endomorphism.Propositional)
+  infixr 8 _^_            (Function.Endomorphism.Setoid)
+  infix  4 _≃_            (Function.HalfAdjointEquivalence)
+  infix  4 _≈_ _≈ᵢ_ _≤_   (Function.Metric.Bundles)
+  infixl 6 _∙_            (Function.Metric.Bundles)
+  infix  4 _≈_            (Function.Metric.Nat.Bundles)
+  infix  3 _←_ _↢_        (Function.Related)
+
   infix  4 _ℕ<_ _ℕ≤infinity _ℕ≤_                            (Codata.Sized.Conat)
   infix  6 _ℕ+_ _+ℕ_                                        (Codata.Sized.Conat)
   infixl 4 _+ _*                                            (Data.List.Kleene.Base)

src/Data/Vec/Functional/Relation/Binary/Equality/Setoid.agda

@@ -24,6 +24,8 @@ open Setoid S renaming (Carrier to A)
 -- Definition
 ------------------------------------------------------------------------
 
+infix 4 _≋_
+
 _≋_ : ∀ {n} → Vector A n → Vector A n → Set ℓ
 _≋_ = Pointwise _≈_
 

src/Data/Vec/N-ary.agda

@@ -45,6 +45,8 @@ curryⁿ : ∀ {n} → (Vec A n → B) → N-ary n A B
 curryⁿ {n = zero}  f = f []
 curryⁿ {n = suc n} f = λ x → curryⁿ (f ∘ _∷_ x)
 
+infix -1 _$ⁿ_
+
 _$ⁿ_ : ∀ {n} → N-ary n A B → (Vec A n → B)
 f $ⁿ []       = f
 f $ⁿ (x ∷ xs) = f x $ⁿ xs

src/Function/Endomorphism/Propositional.agda

@@ -43,6 +43,8 @@ toSetoidEndo f = record
 ------------------------------------------------------------------------
 -- N-th composition
 
+infixr 8 _^_
+
 _^_ : Endo → ℕ → Endo
 f ^ zero  = id
 f ^ suc n = f ∘′ (f ^ n)

src/Function/Endomorphism/Setoid.agda

@@ -35,6 +35,8 @@ private
 Endo : Set _
 Endo = S ⟶ S
 
+infixr 8 _^_
+
 _^_ : Endo → ℕ → Endo
 f ^ zero  = id
 f ^ suc n = f ∘ (f ^ n)

src/Function/HalfAdjointEquivalence.agda

@@ -16,6 +16,8 @@ open import Relation.Binary.PropositionalEquality
 
 -- Half adjoint equivalences (see the HoTT book).
 
+infix 4 _≃_
+
 record _≃_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
   field
     to               : A → B

src/Function/Metric/Bundles.agda

@@ -22,6 +22,7 @@ open import Function.Metric.Core
 
 record ProtoMetric (a i ℓ₁ ℓ₂ ℓ₃ : Level)
                  : Set (suc (a ⊔ i ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃)) where
+  infix 4 _≈_ _≈ᵢ_ _≤_
   field
     Carrier       : Set a
     Image         : Set i
@@ -39,6 +40,7 @@ record ProtoMetric (a i ℓ₁ ℓ₂ ℓ₃ : Level)
 
 record PreMetric (a i ℓ₁ ℓ₂ ℓ₃ : Level)
                : Set (suc (a ⊔ i ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃)) where
+  infix 4 _≈_ _≈ᵢ_ _≤_
   field
     Carrier     : Set a
     Image       : Set i
@@ -61,6 +63,8 @@ record PreMetric (a i ℓ₁ ℓ₂ ℓ₃ : Level)
 
 record QuasiSemiMetric (a i ℓ₁ ℓ₂ ℓ₃ : Level)
                      : Set (suc (a ⊔ i ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃)) where
+
+  infix 4 _≈_ _≈ᵢ_ _≤_
   field
     Carrier           : Set a
     Image             : Set i
@@ -86,6 +90,7 @@ record QuasiSemiMetric (a i ℓ₁ ℓ₂ ℓ₃ : Level)
 
 record SemiMetric (a i ℓ₁ ℓ₂ ℓ₃ : Level)
                 : Set (suc (a ⊔ i ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃)) where
+  infix 4 _≈_ _≈ᵢ_ _≤_
   field
     Carrier      : Set a
     Image        : Set i
@@ -120,6 +125,8 @@ record SemiMetric (a i ℓ₁ ℓ₂ ℓ₃ : Level)
 
 record GeneralMetric (a i ℓ₁ ℓ₂ ℓ₃ : Level)
                    : Set (suc (a ⊔ i ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃)) where
+  infix 4 _≈_ _≈ᵢ_ _≤_
+  infixl 6 _∙_
   field
     Carrier         : Set a
     Image           : Set i

src/Function/Metric/Nat/Bundles.agda

@@ -28,6 +28,7 @@ open import Function.Metric.Bundles as Base
 -- Proto-metric
 
 record ProtoMetric a ℓ : Set (suc (a ⊔ ℓ)) where
+  infix 4 _≈_
   field
     Carrier       : Set a
     _≈_           : Rel Carrier ℓ
@@ -40,6 +41,7 @@ record ProtoMetric a ℓ : Set (suc (a ⊔ ℓ)) where
 -- PreMetric
 
 record PreMetric a ℓ : Set (suc (a ⊔ ℓ)) where
+  infix 4 _≈_
   field
     Carrier     : Set a
     _≈_         : Rel Carrier ℓ
@@ -57,6 +59,7 @@ record PreMetric a ℓ : Set (suc (a ⊔ ℓ)) where
 -- QuasiSemiMetric
 
 record QuasiSemiMetric a ℓ : Set (suc (a ⊔ ℓ)) where
+  infix 4 _≈_
   field
     Carrier           : Set a
     _≈_               : Rel Carrier ℓ
@@ -77,6 +80,7 @@ record QuasiSemiMetric a ℓ : Set (suc (a ⊔ ℓ)) where
 -- SemiMetric
 
 record SemiMetric a ℓ : Set (suc (a ⊔ ℓ)) where
+  infix 4 _≈_
   field
     Carrier      : Set a
     _≈_          : Rel Carrier ℓ
@@ -97,6 +101,7 @@ record SemiMetric a ℓ : Set (suc (a ⊔ ℓ)) where
 -- Metrics
 
 record Metric a ℓ : Set (suc (a ⊔ ℓ)) where
+  infix 4 _≈_
   field
     Carrier  : Set a
     _≈_      : Rel Carrier ℓ
@@ -117,6 +122,7 @@ record Metric a ℓ : Set (suc (a ⊔ ℓ)) where
 -- UltraMetrics
 
 record UltraMetric a ℓ : Set (suc (a ⊔ ℓ)) where
+  infix 4 _≈_
   field
     Carrier       : Set a
     _≈_           : Rel Carrier ℓ

src/Function/Related.agda

@@ -53,6 +53,8 @@ open R public using
 -- (which implies that Agda can deduce the universe code from an
 -- expression matching any of the right-hand sides).
 
+infix 3 _←_ _↢_
+
 record _←_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
   constructor lam
   field app-← : B → A

src/Reflection/AST/Argument/Information.agda

@@ -48,6 +48,8 @@ arg-info-injective₂ refl = refl
 arg-info-injective : arg-info v m ≡ arg-info v′ m′ → v ≡ v′ × m ≡ m′
 arg-info-injective = < arg-info-injective₁ , arg-info-injective₂ >
 
+infix 4 _≟_
+
 _≟_ : DecidableEquality ArgInfo
 arg-info v m ≟ arg-info v′ m′ =
   map′