Algebra fixity (#2386)

* put the fixity recommendations into the style guide

* mixing fixity declaration

* was missing a case

* use the new case

* add fixities for everything in Algebra

* incorporate some suggestions for extra cases

Author: JacquesCarette

doc/README/Design/Fixity.agda

@@ -34,3 +34,4 @@ module README.Design.Fixity where
 -- type formers:
 -- product-like infixr 2 _×_ _-×-_ _-,-_
 -- sum-like infixr 1 _⊎_
+-- binary properties infix 4 _Absorbs_

doc/style-guide.md

@@ -525,6 +525,66 @@ word within a compound word is capitalized except for the first word.
 * Any exceptions to these conventions should be flagged on the GitHub
   `agda-stdlib` issue tracker in the usual way.
 
+#### Fixity
+
+All functions and operators that are not purely prefix (typically
+anything that has a `_` in its name) should have an explicit fixity
+declared for it. The guidelines for these are as follows:
+
+General operations and relations:
+
+* binary relations of all kinds are `infix 4`
+
+* unary prefix relations `infix 4 ε∣_`
+
+* unary postfix relations `infixr 8 _∣0`
+
+* multiplication-like: `infixl 7 _*_`
+
+* addition-like  `infixl 6 _+_`
+
+* arithmetic prefix minus-like  `infix  8 -_`
+
+* arithmetic infix binary minus-like `infixl 6 _-_`
+
+* and-like  `infixr 7 _∧_`
+
+* or-like  `infixr 6 _∨_`
+
+* negation-like `infix 3 ¬_`
+
+* post-fix inverse  `infix  8 _⁻¹`
+
+* bind `infixl 1 _>>=_`
+
+* list concat-like `infixr 5 _∷_`
+
+* ternary reasoning `infix 1 _⊢_≈_`
+
+* composition `infixr 9 _∘_`
+
+* application `infixr -1 _$_ _$!_`
+
+* combinatorics `infixl 6.5 _P_ _P′_ _C_ _C′_`
+
+* pair `infixr 4 _,_`
+
+Reasoning:
+
+* QED  `infix  3 _∎`
+
+* stepping  `infixr 2 _≡⟨⟩_ step-≡ step-≡˘`
+
+* begin  `infix  1 begin_`
+
+Type formers:
+
+* product-like `infixr 2 _×_ _-×-_ _-,-_`
+
+* sum-like `infixr 1 _⊎_`
+
+*  binary properties `infix 4 _Absorbs_`
+
 #### Functions and relations over specific datatypes
 
 * When defining a new relation `P` over a datatype `X` in a `Data.X.Relation` module,

src/Algebra/Bundles.agda

@@ -917,6 +917,7 @@ record NonAssociativeRing c ℓ : Set (suc (c ⊔ ℓ)) where
     using () renaming (magma to *-magma; identity to *-identity)
 
 record Nearring c ℓ : Set (suc (c ⊔ ℓ)) where
+  infix  8 -_
   infixl 7 _*_
   infixl 6 _+_
   infix  4 _≈_

src/Algebra/Definitions.agda

@@ -97,6 +97,8 @@ RightConical e _∙_ = ∀ x y → (x ∙ y) ≈ e → y ≈ e
 Conical : A → Op₂ A → Set _
 Conical e ∙ = (LeftConical e ∙) × (RightConical e ∙)
 
+infix 4 _DistributesOverˡ_ _DistributesOverʳ_ _DistributesOver_
+
 _DistributesOverˡ_ : Op₂ A → Op₂ A → Set _
 _*_ DistributesOverˡ _+_ =
   ∀ x y z → (x * (y + z)) ≈ ((x * y) + (x * z))
@@ -108,6 +110,8 @@ _*_ DistributesOverʳ _+_ =
 _DistributesOver_ : Op₂ A → Op₂ A → Set _
 * DistributesOver + = (* DistributesOverˡ +) × (* DistributesOverʳ +)
 
+infix 4 _MiddleFourExchange_ _IdempotentOn_ _Absorbs_
+
 _MiddleFourExchange_ : Op₂ A → Op₂ A → Set _
 _*_ MiddleFourExchange _+_ =
   ∀ w x y z → ((w + x) * (y + z)) ≈ ((w + y) * (x + z))

src/Algebra/Definitions/RawMagma.agda

@@ -25,7 +25,7 @@ open RawMagma M renaming (Carrier to A)
 ------------------------------------------------------------------------
 -- Divisibility
 
-infix 5 _∣ˡ_ _∤ˡ_ _∣ʳ_ _∤ʳ_ _∣_ _∤_
+infix 5 _∣ˡ_ _∤ˡ_ _∣ʳ_ _∤ʳ_ _∣_ _∤_ _∣∣_ _∤∤_
 
 -- Divisibility from the left.
 --

src/Algebra/Module/Bundles.agda

@@ -279,6 +279,7 @@ record Bimodule (R-ring : Ring r ℓr) (S-ring : Ring s ℓs) m ℓm
     module R = Ring R-ring
     module S = Ring S-ring
 
+  infix 8 -ᴹ_
   infixr 7 _*ₗ_
   infixl 7 _*ᵣ_
   infixl 6 _+ᴹ_

src/Algebra/Module/Definitions/Left.agda

@@ -31,6 +31,8 @@ LeftIdentity a _∙ᴮ_ = ∀ m → (a ∙ᴮ m) ≈ m
 Associative : Op₂ A → Opₗ A B → Set _
 Associative _∙ᴬ_ _∙ᴮ_ = ∀ x y m → ((x ∙ᴬ y) ∙ᴮ m) ≈ (x ∙ᴮ (y ∙ᴮ m))
 
+infix 4 _DistributesOverˡ_ _DistributesOverʳ_⟶_
+
 _DistributesOverˡ_ : Opₗ A B → Op₂ B → Set _
 _*_ DistributesOverˡ _+_ =
   ∀ x m n → (x * (m + n)) ≈ ((x * m) + (x * n))

src/Algebra/Module/Definitions/Right.agda

@@ -31,6 +31,8 @@ RightIdentity a _∙ᴮ_ = ∀ m → (m ∙ᴮ a) ≈ m
 Associative : Op₂ A → Opᵣ A B → Set _
 Associative _∙ᴬ_ _∙ᴮ_ = ∀ m x y → ((m ∙ᴮ x) ∙ᴮ y) ≈ (m ∙ᴮ (x ∙ᴬ y))
 
+infix 4 _DistributesOverʳ_ _DistributesOverˡ_⟶_
+
 _DistributesOverˡ_⟶_ : Opᵣ A B → Op₂ A → Op₂ B → Set _
 _*_ DistributesOverˡ _+ᴬ_ ⟶ _+ᴮ_ =
   ∀ m x y → (m * (x +ᴬ y)) ≈ ((m * x) +ᴮ (m * y))

src/Algebra/Properties/Monoid/Divisibility.agda

@@ -26,6 +26,8 @@ open import Algebra.Properties.Semigroup.Divisibility semigroup public
 ------------------------------------------------------------------------
 -- Additional properties
 
+infix 4 ε∣_
+
 ε∣_ : ∀ x → ε ∣ x
 ε∣ x = x , identityʳ x
 

src/Algebra/Properties/Semiring/Divisibility.agda

@@ -25,6 +25,8 @@ open MonoidDivisibility *-monoid public
 ------------------------------------------------------------------------
 -- Divisibility properties specific to semirings.
 
+infixr 8 _∣0
+
 _∣0 : ∀ x → x ∣ 0#
 x ∣0 = 0# , zeroˡ x
 

src/Algebra/Solver/Ring/AlmostCommutativeRing.agda

@@ -76,6 +76,8 @@ record AlmostCommutativeRing c ℓ : Set (suc (c ⊔ ℓ)) where
 ------------------------------------------------------------------------
 -- Homomorphisms
 
+infix 4 _-Raw-AlmostCommutative⟶_
+
 record _-Raw-AlmostCommutative⟶_
   {r₁ r₂ r₃ r₄}
   (From : RawRing r₁ r₄)