Fixity

CHANGELOG.md

@@ -608,3 +608,43 @@ Other minor additions
   ```agda
   <-isDecStrictPartialOrder : IsDecPartialOrder _≈_ _≤_ → IsDecStrictPartialOrder _≈_ _<_
   ```
+
+* The following operators have had fixities assigneed:
+  ```
+  infix   4 _[_]            (Data.Graph.Acyclic)
+
+  infix   4 _∣?_            (Data.Integer.Divisibility.Signed)
+
+  infix   4 _∈_ _∉_         (Data.List.Fresh.Membership.Setoid)
+  infixr  5 _∷_             (Data.List.Fresh.Relation.Unary.All)
+  infixr  5 _∷_ _++_        (Data.List.Relation.Binary.Prefix.Heterogeneous)
+  infix   4 _⊆?_            (Data.List.Relation.Binary.Sublist.DecSetoid)
+  infix   4  _⊆I_ _⊆R_ _⊆T_ (Data.List.Relation.Binary.Sublist.Heterogeneous.Solver)
+  infixr  8 _⇒_             (Data.List.Relation.Binary.Sublist.Propositional.Example.UniqueBoundVariables)
+  infix   1 _⊢_~_▷_         (Data.List.Relation.Binary.Sublist.Propositional.Example.UniqueBoundVariables)
+  infix   4 _++-mono_       (Data.List.Relation.Binary.Subset.Propositional.Properties)
+  infix   4  _⊛-mono_       (Data.List.Relation.Binary.Subset.Propositional.Properties)
+  infix   4 _⊗-mono_        (Data.List.Relation.Binary.Subset.Propositional.Properties)
+  infixr  5 _++_            (Data.List.Relation.Binary.Suffix.Heterogeneous)
+  infixr  5 _∷ˡ_ _∷ʳ_       (Data.List.Relation.Ternary.Interleaving)
+  infix   1  _++_∷_         (Data.List.Relation.Unary.First)
+  infixr  5 _∷_             (Data.List.Relation.Unary.First)
+
+  infix   4 _≥_             (Data.Nat.Binary.Base)
+  infix   4  _<?_ _≟_ _≤?_  (Data.Nat.Binary.Properties)
+  infixr  1 _∪-Fin_         (Data.Nat.InfinitelyOften)
+
+  infixr -1 _<$>_           (Function.Nary.NonDependent.Base)
+  infix   1 _%=_⊢_          (Function.Nary.NonDependent.Base)
+  infix   1 _∷=_⊢_          (Function.Nary.NonDependent.Base)
+
+  infixr  2 _⊗_             (Induction.Lexicographic)
+
+  infix  10 _⋆              (Relation.Binary.Construct.Closure.ReflexiveTransitive)
+  infix   4  _≤_            (Relation.Binary.Construct.StrictToNonStrict)
+
+  infixr  6 _$ʳ_            (Tactic.RingSolver)
+  infix  -1 _$ᵉ_            (Tactic.RingSolver)
+  infix   4 _⇓≟_            (Tactic.RingSolver)
+  infixl  6 _⊜_             (Tactic.RingSolver.NonReflective)
+  ```

README/Design/Fixity.agda

@@ -0,0 +1,34 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Documentation describing some of the fixity choices
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+-- There is no actual code in here, just design note.
+
+module README.Design.Fixity where
+
+
+-- binary relations of all kinds are infix 4
+-- multiplication-like: infixl 7 _*_
+-- addition-like  infixl 6 _+_
+-- negation-like  infix  8 ¬_
+-- and-like  infixr 7 _∧_
+-- or-like  infixr 6 _∨_
+-- post-fix inverse  infix  8 _⁻¹
+-- bind infixl 1 _>>=_
+-- list concat-like infixr 5 _∷_
+-- ternary reasoning infix 1 _⊢_≈_
+-- composition infixr 9 _∘_
+-- application infixr -1 _$_ _$!_
+
+-- Reasoning:
+-- QED  infix  3 _∎
+-- stepping  infixr 2 _≡⟨⟩_ step-≡ step-≡˘
+-- begin  infix  1 begin_
+
+-- type formers:
+-- product-like infixr 2 _×_ _-×-_ _-,-_
+-- sum-like infixr 1 _⊎_

src/Data/Graph/Acyclic.agda

@@ -170,6 +170,8 @@ module _ {ℓ e} {N : Set ℓ} {E : Set e} where
 -- Finds the context and remaining graph corresponding to a given node
 -- index.
 
+  infix 4 _[_]
+
   _[_] : ∀ {n} → Graph N E n → (i : Fin n) → Graph N E (suc (n - suc i))
   (c & g) [ zero ]  = c & g
   (c & g) [ suc i ] = g [ i ]

src/Data/Integer/Divisibility/Signed.agda

@@ -127,6 +127,8 @@ module ∣-Reasoning where
 ------------------------------------------------------------------------
 -- Other properties of _∣_
 
+infix 4 _∣?_
+
 _∣?_ : Decidable _∣_
 k ∣? m = DEC.map′ ∣ᵤ⇒∣ ∣⇒∣ᵤ (∣ k ∣ ℕ.∣? ∣ m ∣)
 

src/Data/List/Fresh/Membership/Setoid.agda

@@ -17,6 +17,8 @@ open import Relation.Nullary
 
 open Setoid S renaming (Carrier to A)
 
+infix 4 _∈_ _∉_
+
 private
   variable
     r : Level

src/Data/List/Fresh/Relation/Unary/All.agda

@@ -26,6 +26,8 @@ private
 
 module _ {A : Set a} {R : Rel A r} (P : Pred A p) where
 
+  infixr 5 _∷_
+
   data All : List# A R → Set (p ⊔ a ⊔ r) where
     []  : All []
     _∷_ : ∀ {x xs pr} → P x → All xs → All (cons x xs pr)

src/Data/List/Relation/Binary/Prefix/Heterogeneous.agda

@@ -17,6 +17,8 @@ open import Relation.Binary using (REL; _⇒_)
 
 module _ {a b r} {A : Set a} {B : Set b} (R : REL A B r) where
 
+  infixr 5 _∷_ _++_
+
   data Prefix : REL (List A) (List B) (a ⊔ b ⊔ r) where
     []  : ∀ {bs} → Prefix [] bs
     _∷_ : ∀ {a b as bs} → R a b → Prefix as bs → Prefix (a ∷ as) (b ∷ bs)

src/Data/List/Relation/Binary/Sublist/DecSetoid.agda

@@ -22,6 +22,8 @@ open import Level using (_⊔_)
 open DecSetoid S
 open DecSetoidEquality S
 
+infix 4 _⊆?_
+
 ------------------------------------------------------------------------
 -- Re-export core definitions
 

src/Data/List/Relation/Binary/Sublist/Heterogeneous/Solver.agda

@@ -37,6 +37,8 @@ open import Relation.Nullary
 
 open P.≡-Reasoning
 
+infix 4  _⊆I_ _⊆R_ _⊆T_
+
 ------------------------------------------------------------------------
 -- Reified list expressions
 

src/Data/List/Relation/Binary/Sublist/Propositional/Example/UniqueBoundVariables.agda

@@ -38,6 +38,9 @@ open import Data.List.Relation.Binary.Sublist.Propositional.Properties using
 
 open import Data.Product using (_,_; proj₁; proj₂)
 
+infixr 8 _⇒_
+infix 1 _⊢_~_▷_
+
 -- Simple types over a set Base of base types.
 
 data Ty : Set where

src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda

@@ -101,6 +101,7 @@ module _ {a b} {A : Set a} {B : Set b} (f : A → B) {xs ys} where
 -- _++_
 
 module _ {a} {A : Set a} {xs₁ xs₂ ys₁ ys₂ : List A} where
+  infix 4 _++-mono_
 
   _++-mono_ : xs₁ ⊆ ys₁ → xs₂ ⊆ ys₂ → xs₁ ++ xs₂ ⊆ ys₁ ++ ys₂
   _++-mono_ xs₁⊆ys₁ xs₂⊆ys₂ =
@@ -134,6 +135,7 @@ module _ {ℓ} {A B : Set ℓ} (f g : A → List B) {xs ys} where
 -- _⊛_
 
 module _ {ℓ} {A B : Set ℓ} {fs gs : List (A → B)} {xs ys : List A} where
+  infix 4  _⊛-mono_
 
   _⊛-mono_ : fs ⊆ gs → xs ⊆ ys → (fs ⊛ xs) ⊆ (gs ⊛ ys)
   _⊛-mono_ fs⊆gs xs⊆ys =
@@ -145,6 +147,7 @@ module _ {ℓ} {A B : Set ℓ} {fs gs : List (A → B)} {xs ys : List A} where
 -- _⊗_
 
 module _ {ℓ} {A B : Set ℓ} {xs₁ ys₁ : List A} {xs₂ ys₂ : List B} where
+  infix 4 _⊗-mono_
 
   _⊗-mono_ : xs₁ ⊆ ys₁ → xs₂ ⊆ ys₂ → (xs₁ ⊗ xs₂) ⊆ (ys₁ ⊗ ys₂)
   xs₁⊆ys₁ ⊗-mono xs₂⊆ys₂ =

src/Data/List/Relation/Binary/Suffix/Heterogeneous.agda

@@ -16,6 +16,8 @@ open import Data.List.Relation.Binary.Pointwise as Pointwise
 
 module _ {a b r} {A : Set a} {B : Set b} (R : REL A B r) where
 
+  infixr 5 _++_
+
   data Suffix : REL (List A) (List B) (a ⊔ b ⊔ r) where
     here  : ∀ {as bs} → Pointwise R as bs → Suffix as bs
     there : ∀ {b as bs} → Suffix as bs → Suffix as (b ∷ bs)

src/Data/List/Relation/Ternary/Interleaving.agda

@@ -24,6 +24,8 @@ open import Relation.Binary.PropositionalEquality as P using (_≡_)
 module _ {a b c l r} {A : Set a} {B : Set b} {C : Set c}
          (L : REL A C l) (R : REL B C r) where
 
+  infixr 5 _∷ˡ_ _∷ʳ_
+
   data Interleaving : List A → List B → List C → Set (a ⊔ b ⊔ c ⊔ l ⊔ r) where
     []   : Interleaving [] [] []
     _∷ˡ_ : ∀ {a c l r cs} → L a c → Interleaving l r cs → Interleaving (a ∷ l) r (c ∷ cs)

src/Data/List/Relation/Unary/First.agda

@@ -26,6 +26,9 @@ open import Relation.Nullary
 
 module _ {p q} (P : Pred A p) (Q : Pred A q) where
 
+  infix 1 _++_∷_
+  infixr 5 _∷_
+
   data First : Pred (List A) (a ⊔ p ⊔ q) where
     [_] : ∀ {x xs} → Q x            → First (x ∷ xs)
     _∷_ : ∀ {x xs} → P x → First xs → First (x ∷ xs)

src/Data/Nat/Binary/Base.agda

@@ -32,7 +32,7 @@ data ℕᵇ : Set where
 ------------------------------------------------------------------------
 -- Ordering relations
 
-infix 4 _<_ _>_ _≤_ _≮_ _≯_ _≰_ _≱_
+infix 4 _<_ _>_ _≤_ _≥_ _≮_ _≯_ _≰_ _≱_
 
 data _<_ : Rel ℕᵇ 0ℓ  where
   0<even    : ∀ {x} → zero < 2[1+ x ]

src/Data/Nat/Binary/Properties.agda

@@ -41,6 +41,8 @@ import Relation.Binary.Construct.StrictToNonStrict _≡_ _<_
   as StrictToNonStrict
 open +-*-Solver
 
+infix 4  _<?_ _≟_ _≤?_
+
 ------------------------------------------------------------------------
 -- Properties of _≡_
 ------------------------------------------------------------------------

src/Data/Nat/InfinitelyOften.agda

@@ -22,6 +22,8 @@ open import Relation.Nullary.Negation using (¬¬-Monad; call/cc)
 open import Relation.Unary using (Pred; _∪_; _⊆_)
 open RawMonad (¬¬-Monad {p = 0ℓ})
 
+infixr 1 _∪-Fin_
+
 -- Only true finitely often.
 
 Fin : ∀ {ℓ} → Pred ℕ ℓ → Set ℓ

src/Function/Nary/NonDependent/Base.agda

@@ -85,10 +85,12 @@ _⇉_ = Arrows _
 
 -- Level-respecting map
 
+infixr -1 _<$>_
+
 _<$>_ : (∀ {l} → Set l → Set l) →
         ∀ {n ls} → Sets n ls → Sets n ls
 _<$>_ f {zero}   as        = _
-_<$>_ f {suc n}  (a , as)  = f a , f <$> as
+_<$>_ f {suc n}  (a , as)  = f a , (f <$> as)
 
 -- Level-modifying generalised map
 
@@ -112,11 +114,15 @@ mapₙ (suc n) f g = mapₙ n f ∘′ g
 
 -- compose function at the n-th position
 
+infix 1 _%=_⊢_
+
 _%=_⊢_ : ∀ n {ls} {as : Sets n ls} → (A → B) → as ⇉ (B → C) → as ⇉ (A → C)
 n %= f ⊢ g = mapₙ n (_∘′ f) g
 
 -- partially apply function at the n-th position
 
+infix 1 _∷=_⊢_
+
 _∷=_⊢_ : ∀ n {ls} {as : Sets n ls} → A → as ⇉ (A → B) → as ⇉ B
 n ∷= x ⊢ g = mapₙ n (_$′ x) g
 

src/Induction/Lexicographic.agda

@@ -24,6 +24,8 @@ open import Level
   -- ...or x is "smaller" and y is arbitrary.
   RecA (λ x′ → ∀ y′ → P (x′ , y′)) x
 
+infixr 2 _⊗_
+
 _⊗_ : ∀ {a b ℓ₁ ℓ₂ ℓ₃} {A : Set a} {B : Set b} →
       RecStruct A (ℓ₁ ⊔ b) ℓ₂ → RecStruct B ℓ₁ ℓ₃ →
       RecStruct (A × B) _ _

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

@@ -115,14 +115,16 @@ kleisliStar : ∀ {i j t u}
               (f : I → J) → T =[ f ]⇒ Star U → Star T =[ f ]⇒ Star U
 kleisliStar f g = concat ∘′ gmap f g
 
+infix 10 _⋆
+
 _⋆ : ∀ {i t u} {I : Set i} {T : Rel I t} {U : Rel I u} →
      T ⇒ Star U → Star T ⇒ Star U
 _⋆ = kleisliStar id
 
 infixl 1 _>>=_
 
-_>>=_ : ∀ {i t u} {I : Set i} {T : Rel I t} {U : Rel I u} {i j} →
-        Star T i j → T ⇒ Star U → Star U i j
+_>>=_ : ∀ {i t u} {I : Set i} {T : Rel I t} {U : Rel I u} {j k} →
+        Star T j k → T ⇒ Star U → Star U j k
 m >>= f = (f ⋆) m
 
 -- Note that the monad-like structure above is not an indexed monad

src/Relation/Binary/Construct/StrictToNonStrict.agda

@@ -29,6 +29,7 @@ open import Relation.Nullary.Sum using (_⊎-dec_)
 -- Conversion
 
 -- _<_ can be turned into _≤_ as follows:
+infix 4  _≤_
 
 _≤_ : Rel A _
 x ≤ y = (x < y) ⊎ (x ≈ y)

src/Tactic/RingSolver.agda

@@ -61,6 +61,8 @@ private
     -- explicit argument and the terms of it's arguments and inserts
     -- the required ring arguments
     --   e.g. "_+_" $ʳ xs = "_+_ {_} {_} ring xs"
+    infixr 6 _$ʳ_
+
     _$ʳ_ : Name → Args Term → Term
     nm $ʳ args = def nm (2 ⋯⟅∷⟆ ring ⟨∷⟩ args)
 
@@ -89,13 +91,15 @@ private
       -- type it contains, and the third is the number of variables it's
       -- indexed by. All three of these could likely be inferred, but to
       -- make things easier we supply the third because we know it.
+      infix -1 _$ᵉ_
       _$ᵉ_ : Name → List (Arg Term) → Term
       e $ᵉ xs = con e (1 ⋯⟅∷⟆ quote Carrier $ʳ [] ⟅∷⟆ toTerm numVars ⟅∷⟆ xs)
 
       -- A constant expression.
       Κ′ : Term → Term
       Κ′ x = quote Κ $ᵉ (x ⟨∷⟩ [])
 
+      infix 4 _⇓≟_
       _⇓≟_ : Maybe Name → Name → Bool
       nothing ⇓≟ _ = false
       just x  ⇓≟ y = primQNameEquality x y

src/Tactic/RingSolver/NonReflective.agda

@@ -93,6 +93,7 @@ solve : ∀ (n : ℕ) →
 solve = Ops.solve
 {-# INLINE solve #-}
 
+infixl 6 _⊜_
 _⊜_ : ∀ {n : ℕ} →
       Expr Carrier n →
       Expr Carrier n →