Improve fixity declarations (#1228)

Author: JacquesCarette

CHANGELOG.md

@@ -651,3 +651,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