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′

src/Reflection/AST/Argument/Modality.agda

@@ -48,6 +48,8 @@ modality-injective₂ refl = refl
 modality-injective : modality r q ≡ modality r′ q′ → r ≡ r′ × q ≡ q′
 modality-injective = < modality-injective₁ , modality-injective₂ >
 
+infix 4 _≟_
+
 _≟_ : DecidableEquality Modality
 modality r q ≟ modality r′ q′ =
   map′

src/Reflection/AST/Argument/Quantity.agda

@@ -21,6 +21,8 @@ open Quantity public
 ------------------------------------------------------------------------
 -- Decidable equality
 
+infix 4 _≟_
+
 _≟_ : DecidableEquality Quantity
 quantity-ω ≟ quantity-ω = yes refl
 quantity-0 ≟ quantity-0 = yes refl

src/Reflection/AST/Argument/Relevance.agda

@@ -21,6 +21,8 @@ open Relevance public
 ------------------------------------------------------------------------
 -- Decidable equality
 
+infix 4 _≟_
+
 _≟_ : DecidableEquality Relevance
 relevant   ≟ relevant   = yes refl
 irrelevant ≟ irrelevant = yes refl

src/Reflection/AST/Argument/Visibility.agda

@@ -21,6 +21,8 @@ open Visibility public
 ------------------------------------------------------------------------
 -- Decidable equality
 
+infix 4 _≟_
+
 _≟_ : DecidableEquality Visibility
 visible   ≟ visible   = yes refl
 hidden    ≟ hidden    = yes refl

src/Reflection/AST/Definition.agda

@@ -59,6 +59,8 @@ record′-injective = < record′-injective₁ , record′-injective₂ >
 constructor′-injective : ∀ {c c′} → constructor′ c ≡ constructor′ c′ → c ≡ c′
 constructor′-injective refl = refl
 
+infix 4 _≟_
+
 _≟_ : DecidableEquality Definition
 function cs       ≟ function cs′        =
   map′ (cong function) function-injective (cs Term.≟-Clauses cs′)

src/Reflection/AST/Literal.agda

@@ -104,5 +104,7 @@ meta x ≟ string x₁ = no (λ ())
 meta x ≟ name x₁ = no (λ ())
 meta x ≟ meta x₁ = map′ (cong meta) meta-injective (x Meta.≟ x₁)
 
+infix 4 _≡ᵇ_
+
 _≡ᵇ_ : Literal → Literal → Bool
 l ≡ᵇ l′ = isYes (l ≟ l′)

src/Reflection/AST/Meta.agda

@@ -23,12 +23,13 @@ open import Agda.Builtin.Reflection.Properties public
 
 -- Equality of metas is decidable.
 
+infix 4 _≈?_ _≟_ _≈_
+
 _≈_ : Rel Meta _
 _≈_ = _≡_ on toℕ
 
 _≈?_ : Decidable _≈_
 _≈?_ = On.decidable toℕ _≡_ ℕₚ._≟_
 
-infix 4 _≟_
 _≟_ : DecidableEquality Meta
 m ≟ n = map′ (toℕ-injective _ _) (cong toℕ) (m ≈? n)

src/Reflection/AST/Name.agda

@@ -37,11 +37,11 @@ Names = List Name
 -- Decidable equality for names
 ----------------------------------------------------------------------
 
+infix 4 _≈?_ _≟_ _≈_
+
 _≈_ : Rel Name _
 _≈_ = _≡_ on toWords
 
-infix 4 _≈?_ _≟_
-
 _≈?_ : Decidable _≈_
 _≈?_ = decidable toWords _≡_ (Prodₚ.≡-dec Wₚ._≟_ Wₚ._≟_)
 

src/Reflection/AST/Term.agda

@@ -128,7 +128,7 @@ absurd-clause-injective = < absurd-clause-injective₁ , absurd-clause-injective
 
 infix 4 _≟-AbsTerm_ _≟-AbsType_ _≟-ArgTerm_ _≟-ArgType_ _≟-Args_
         _≟-Clause_ _≟-Clauses_ _≟_
-        _≟-Sort_ _≟-Pattern_ _≟-Patterns_
+        _≟-Sort_ _≟-Pattern_ _≟-Patterns_ _≟-Telescope_
 
 _≟-AbsTerm_  : DecidableEquality (Abs Term)
 _≟-AbsType_  : DecidableEquality (Abs Type)