Include CHANGELOG in fix-whitespace and whitespace fixes

CHANGELOG.md

@@ -170,7 +170,7 @@ Additions to existing modules
   quasigroup      : Quasigroup _ _
   isLoop          : IsLoop _∙_ _\\_ _//_ ε
   loop            : Loop _ _
-  
+
   \\-leftDividesˡ  : LeftDividesˡ _∙_ _\\_
   \\-leftDividesʳ  : LeftDividesʳ _∙_ _\\_
   \\-leftDivides   : LeftDivides _∙_ _\\_
@@ -189,7 +189,7 @@ Additions to existing modules
   identityʳ-unique : x ∙ y ≈ x → y ≈ ε
   identity-unique  : Identity x _∙_ → x ≈ ε
   ```
- 
+
 * In `Algebra.Construct.Terminal`:
   ```agda
   rawNearSemiring : RawNearSemiring c ℓ
@@ -218,7 +218,7 @@ Additions to existing modules
   _\\_ : Op₂ A
   x \\ y = (x ⁻¹) ∙ y
   ```
- 
+
 * In `Data.Container.Indexed.Core`:
   ```agda
   Subtrees o c = (r : Response c) → X (next c r)
@@ -327,7 +327,7 @@ Additions to existing modules
   pred-injective : .{{NonZero m}} → .{{NonZero n}} → pred m ≡ pred n → m ≡ n
   pred-cancel-≡ : pred m ≡ pred n → ((m ≡ 0 × n ≡ 1) ⊎ (m ≡ 1 × n ≡ 0)) ⊎ m ≡ n
   ```
-  
+
 * Added new proofs to `Data.Nat.Primality`:
   ```agda
   rough∧square>⇒prime : .{{NonTrivial n}} → m Rough n → m * m > n → Prime n

CHANGELOG/v2.0.md

@@ -38,7 +38,7 @@ Bug-fixes
   Consequently this field has been removed from the record, and the record
   `IsRingWithoutAnnihilatingZero` in `Algebra.Structures.Biased` has been
   deprecated as it is now identical to is `IsRing`.
-  
+
 * In `Algebra.Definitions.RawSemiring` the record `Prime` did not
   enforce that the number was not divisible by `1#`. To fix this
   `p∤1 : p ∤ 1#` has been added as a field.
@@ -212,7 +212,7 @@ Non-backwards compatible changes
 
 * Added new aliases `Is(Meet/Join)(Bounded)Semilattice` for `Is(Bounded)Semilattice`
   which can be used to indicate meet/join-ness of the original structures, and
-  the field names in `IsSemilattice` and `Semilattice` have been renamed from 
+  the field names in `IsSemilattice` and `Semilattice` have been renamed from
   `∧-cong` to `∙-cong`to indicate their undirected nature.
 
 * Finally, the following auxiliary files have been moved:
@@ -763,10 +763,10 @@ Non-backwards compatible changes
    - The records in  `Function.Structures` and `Function.Bundles` export proofs
          of these under the names `strictlySurjective`, `strictlyInverseˡ` and
          `strictlyInverseʳ`,
-   - Conversion functions for the definitions have been added in both directions 
-		 to `Function.Consequences(.Propositional/Setoid)`.
-   - Conversion functions for structures have been added in 
-		 `Function.Structures.Biased`.
+   - Conversion functions for the definitions have been added in both directions
+                 to `Function.Consequences(.Propositional/Setoid)`.
+   - Conversion functions for structures have been added in
+                 `Function.Structures.Biased`.
 
 ### New `Function.Strict`
 
@@ -852,9 +852,9 @@ Non-backwards compatible changes
 
   4. The modules `Relation.Nullary.(Product/Sum/Implication)` have been deprecated
          and their contents moved to `Relation.Nullary.(Negation/Reflects/Decidable)`.
-		 
+
   5. The proof `T?` has been moved from `Data.Bool.Properties` to `Relation.Nullary.Decidable.Core`
-	 (but is still re-exported by the former).
+         (but is still re-exported by the former).
 
   as well as the following breaking changes:
 
@@ -1214,7 +1214,7 @@ Other major improvements
 
 * We have then moved raw bundles defined in `Data.X.Properties` to `Data.X.Base` for
   `X` = `Nat`/`Nat.Binary`/`Integer`/`Rational`/`Rational.Unnormalised`.
-  
+
 ### Upgrades to `README` sub-library
 
 * The `README` sub-library has been moved to `doc/README` and a new `doc/standard-library-doc.agda-lib` has been added.
@@ -1223,7 +1223,7 @@ Other major improvements
   using an out-of-the-box standard Agda installation without altering the main
   `standard-library.agda-lib` file.
 
-* The second is that the `README` files are now their own first-class library 
+* The second is that the `README` files are now their own first-class library
   and can be imported like an other library.
 
 Deprecated modules

HACKING.md

@@ -31,7 +31,7 @@ Note on contributions to related/'coupled' modules
 ==================================================
 
 Before making changes to a `Data` module please have a look at related modules
-and see if they have any content along similar lines. If so, then please 
+and see if they have any content along similar lines. If so, then please
 follow those conventions (e.g. naming, argument order).
 For example, if working on `Data.Rational`, please check `Data.Rational.Unnormalised`
 or if working on `Data.Vec` please check `Data.List` and vice versa.

fix-whitespace.yaml

@@ -7,5 +7,4 @@ included-files:
   - "*.md"
 
 excluded-files:
-  - "README/Text/Tabular.agda"
-  - CHANGELOG.md
+  - "README/Text/Tabular.agda"

src/Algebra/Module/Bundles/Raw.agda

@@ -200,7 +200,7 @@ record RawBimodule (R : Set r) (S : Set s) m ℓm : Set (r ⊔ s ⊔ suc (m ⊔
     ; 0ᴹ = 0ᴹ
     ; -ᴹ_ = -ᴹ_
     }
- 
+
   rawRightModule : RawRightModule S m ℓm
   rawRightModule = record
     { _≈ᴹ_ = _≈ᴹ_

src/Algebra/Morphism/Construct/Initial.agda

@@ -39,7 +39,7 @@ zero ()
 -- Basic properties
 
 cong : (≈ : Rel A ℓm) → Rel.Homomorphic₂ ℤero.Carrier A ℤero._≈_ ≈ zero
-cong _ {x = ()} 
+cong _ {x = ()}
 
 injective : (≈ : Rel A ℓm) → Injective ℤero._≈_ ≈ zero
 injective _ {x = ()}
@@ -52,7 +52,7 @@ isMagmaHomomorphism : (M : RawMagma m ℓm) →
 isMagmaHomomorphism M = record
   { isRelHomomorphism = record { cong = cong (RawMagma._≈_ M) }
   ; homo = λ()
-  } 
+  }
 
 isMagmaMonomorphism : (M : RawMagma m ℓm) →
                       IsMagmaMonomorphism rawMagma M zero

src/Data/List/Relation/Ternary/Appending/Setoid/Properties.agda

@@ -23,7 +23,7 @@ open import Relation.Binary.PropositionalEquality.Core using (refl)
 open import Relation.Binary.Construct.Composition using (_;_)
 
 open Setoid S renaming (Carrier to A)
-open import Relation.Binary.Properties.Setoid S using (≈;≈⇒≈; ≈⇒≈;≈)  
+open import Relation.Binary.Properties.Setoid S using (≈;≈⇒≈; ≈⇒≈;≈)
 open import Data.List.Relation.Ternary.Appending.Setoid S
 
 private

src/Data/Nat/Primality/Factorisation.agda

@@ -34,7 +34,7 @@ open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans
 private
   variable
     n : ℕ
-    
+
 ------------------------------------------------------------------------
 -- Core definition
 
@@ -107,18 +107,18 @@ factorise n₀@(2+ _) = build [ <-recBuilder ⊗ <-recBuilder ] P facRec (n₀ ,
         pred (m * m) <⟨ s<s⁻¹ (m∸n≢0⇒n<m λ eq′ → 0≢1+n (trans (sym eq′) eq)) ⟩
         n            ∎
         where open ≤-Reasoning
-        
+
       q = quotient m∣n
-      
+
       instance _  = n>1⇒nonTrivial (quotient>1 m∣n m<n)
-      
+
       factorisation[q] : PrimeFactorisation q
       factorisation[q] = recQuotient (quotient-< m∣n) (suc q ∸ m * m) (rough∧∣⇒rough rough (quotient-∣ m∣n)) refl
-      
+
       ps = factors factorisation[q]
-      
+
       primes = factorsPrime factorisation[q]
-      
+
       m*Πps≡n : m * product ps ≡ n
       m*Πps≡n = begin
         m * product ps ≡⟨ cong (m *_) (isFactorisation factorisation[q]) ⟨