CHANGELOG: fix whitespace violations: replace tabs by spaces

Author: andreasabel

CHANGELOG.md

@@ -371,42 +371,42 @@ Non-backwards compatible changes
   `m / n` without having to explicitly provide a proof, as instance search will fill it in
   for you. The full list of such operations changed is as follows:
     - In `Data.Nat.DivMod`: `_/_`, `_%_`, `_div_`, `_mod_`
-	- In `Data.Nat.Pseudorandom.LCG`: `Generator`
-	- In `Data.Integer.DivMod`: `_divℕ_`, `_div_`, `_modℕ_`, `_mod_`
-	- In `Data.Rational`: `mkℚ+`, `normalize`, `_/_`, `1/_`
-	- In `Data.Rational.Unnormalised`: `_/_`, `1/_`, `_÷_`
+    - In `Data.Nat.Pseudorandom.LCG`: `Generator`
+    - In `Data.Integer.DivMod`: `_divℕ_`, `_div_`, `_modℕ_`, `_mod_`
+    - In `Data.Rational`: `mkℚ+`, `normalize`, `_/_`, `1/_`
+    - In `Data.Rational.Unnormalised`: `_/_`, `1/_`, `_÷_`
 
 * At the moment, there are 4 different ways such instance arguments can be provided,
   listed in order of convenience and clarity:
     1. *Automatic basic instances* - the standard library provides instances based on the constructors of each
-	   numeric type in `Data.X.Base`. For example, `Data.Nat.Base` constains an instance of `NonZero (suc n)` for any `n`
-	   and `Data.Integer.Base` contains an instance of `NonNegative (+ n)` for any `n`. Consequently,
-	   if the argument is of the required form, these instances will always be filled in by instance search
-	   automatically, e.g.
-	   ```
-	   0/n≡0 : 0 / suc n ≡ 0
-	   ```
-	2. *Take the instance as an argument* - You can provide the instance argument as a parameter to your function
-	   and Agda's instance search will automatically use it in the correct place without you having to
-	   explicitly pass it, e.g.
-	   ```
-	   0/n≡0 : .{{_ : NonZero n}} → 0 / n ≡ 0
-	   ```
-	3. *Define the instance locally* - You can define an instance argument in scope (e.g. in a `where` clause)
-	   and Agda's instance search will again find it automatically, e.g.
-	   ```
-	   instance
-	     n≢0 : NonZero n
-	     n≢0 = ...
-
-	   0/n≡0 : 0 / n ≡ 0
-	   ```
-	4. *Pass the instance argument explicitly* - Finally, if all else fails you can pass the
-	   instance argument explicitly into the function using `{{ }}`, e.g.
-	   ```
-	   0/n≡0 : ∀ n (n≢0 : NonZero n) → ((0 / n) {{n≢0}}) ≡ 0
-	   ```
-	   Suitable constructors for `NonZero`/`Positive` etc. can be found in `Data.X.Base`.
+       numeric type in `Data.X.Base`. For example, `Data.Nat.Base` constains an instance of `NonZero (suc n)` for any `n`
+       and `Data.Integer.Base` contains an instance of `NonNegative (+ n)` for any `n`. Consequently,
+       if the argument is of the required form, these instances will always be filled in by instance search
+       automatically, e.g.
+       ```
+       0/n≡0 : 0 / suc n ≡ 0
+       ```
+    2. *Take the instance as an argument* - You can provide the instance argument as a parameter to your function
+       and Agda's instance search will automatically use it in the correct place without you having to
+       explicitly pass it, e.g.
+       ```
+       0/n≡0 : .{{_ : NonZero n}} → 0 / n ≡ 0
+       ```
+    3. *Define the instance locally* - You can define an instance argument in scope (e.g. in a `where` clause)
+       and Agda's instance search will again find it automatically, e.g.
+       ```
+       instance
+         n≢0 : NonZero n
+         n≢0 = ...
+
+       0/n≡0 : 0 / n ≡ 0
+       ```
+    4. *Pass the instance argument explicitly* - Finally, if all else fails you can pass the
+       instance argument explicitly into the function using `{{ }}`, e.g.
+       ```
+       0/n≡0 : ∀ n (n≢0 : NonZero n) → ((0 / n) {{n≢0}}) ≡ 0
+       ```
+       Suitable constructors for `NonZero`/`Positive` etc. can be found in `Data.X.Base`.
 
 * A full list of proofs that have changed to use instance arguments is available at the end of this file.
   Notable changes to proofs are now discussed below.
@@ -457,14 +457,14 @@ Non-backwards compatible changes
 * As a consequence of this, some proofs that relied on this reduction behaviour
   or on eta-equality may no longer go through. There are several ways to fix this:
   1. The principled way is to not rely on this reduction behaviour in the first place.
-	 The `Properties` files for rational numbers have been greatly expanded in `v1.7`
-	 and `v2.0`, and we believe most proofs should be able to be built up from existing
-	 proofs contained within these files.
+     The `Properties` files for rational numbers have been greatly expanded in `v1.7`
+     and `v2.0`, and we believe most proofs should be able to be built up from existing
+     proofs contained within these files.
   2. Alternatively, annotating any rational arguments to a proof with either
-	 `@record{}` or `@(mkℚ _ _ _)` should restore the old reduction behaviour for any
-	 terms involving those parameters.
+     `@record{}` or `@(mkℚ _ _ _)` should restore the old reduction behaviour for any
+     terms involving those parameters.
   3. Finally, if the above approaches are not viable then you may be forced to explicitly
-	 use `cong` combined with a lemma that proves the old reduction behaviour.
+     use `cong` combined with a lemma that proves the old reduction behaviour.
 
 ### Change to the definition of `LeftCancellative` and `RightCancellative`
 
@@ -478,20 +478,20 @@ Non-backwards compatible changes
 
 * Therefore the definitions have been changed as follows to make all their arguments explicit:
   - `LeftCancellative _•_`
-	- From: `∀ x {y z} → (x • y) ≈ (x • z) → y ≈ z`
-	- To: `∀ x y z → (x • y) ≈ (x • z) → y ≈ z`
+    - From: `∀ x {y z} → (x • y) ≈ (x • z) → y ≈ z`
+    - To: `∀ x y z → (x • y) ≈ (x • z) → y ≈ z`
 
   - `RightCancellative _•_`
     - From: `∀ {x} y z → (y • x) ≈ (z • x) → y ≈ z`
-	- To: `∀ x y z → (y • x) ≈ (z • x) → y ≈ z`
+    - To: `∀ x y z → (y • x) ≈ (z • x) → y ≈ z`
 
   - `AlmostLeftCancellative e _•_`
     - From: `∀ {x} y z → ¬ x ≈ e → (x • y) ≈ (x • z) → y ≈ z`
-	- To: `∀ x y z → ¬ x ≈ e → (x • y) ≈ (x • z) → y ≈ z`
+    - To: `∀ x y z → ¬ x ≈ e → (x • y) ≈ (x • z) → y ≈ z`
 
   - `AlmostRightCancellative e _•_`
-	- From: `∀ {x} y z → ¬ x ≈ e → (y • x) ≈ (z • x) → y ≈ z`
-	- To: `∀ x y z → ¬ x ≈ e → (y • x) ≈ (z • x) → y ≈ z`
+    - From: `∀ {x} y z → ¬ x ≈ e → (y • x) ≈ (z • x) → y ≈ z`
+    - To: `∀ x y z → ¬ x ≈ e → (y • x) ≈ (z • x) → y ≈ z`
 
 * Correspondingly some proofs of the above types will need additional arguments passed explicitly.
   Instances can easily be fixed by adding additional underscores, e.g.
@@ -643,7 +643,7 @@ Non-backwards compatible changes
   - `¬?` has been moved from `Relation.Nullary.Negation.Core` to `Relation.Nullary.Decidable.Core`
   - `¬-reflects` has been moved from `Relation.Nullary.Negation.Core` to `Relation.Nullary.Reflects`.
   - `decidable-stable`, `excluded-middle` and `¬-drop-Dec` have been moved from `Relation.Nullary.Negation`
-	to `Relation.Nullary.Decidable`.
+    to `Relation.Nullary.Decidable`.
   - `fromDec` and `toDec` have been mvoed from `Data.Sum.Base` to `Data.Sum`.
 
 ### Refactoring of the unindexed Functor/Applicative/Monad hiearchy
@@ -883,13 +883,13 @@ Major improvements
 
 * The ring solver tactic has been greatly improved. In particular:
   1. When the solver is used for concrete ring types, e.g. ℤ, the equality can now use
-	 all the ring operations defined natively for that type, rather than having
-	 to use the operations defined in `AlmostCommutativeRing`. For example
-	 previously you could not use `Data.Integer.Base._*_` but instead had to
-	 use `AlmostCommutativeRing._*_`.
+     all the ring operations defined natively for that type, rather than having
+     to use the operations defined in `AlmostCommutativeRing`. For example
+     previously you could not use `Data.Integer.Base._*_` but instead had to
+     use `AlmostCommutativeRing._*_`.
   2. The solver now supports use of the subtraction operator `_-_` whenever
      it is defined immediately in terms of `_+_` and `-_`. This is the case for
-	 `Data.Integer` and `Data.Rational`.
+     `Data.Integer` and `Data.Rational`.
 
 ### Moved `_%_` and `_/_` operators to `Data.Nat.Base`