Normalize whitespace everywhere

Author: jespercockx

.github/workflows/nix-ci.yml

@@ -63,4 +63,4 @@ jobs:
     - name: drop into the devshell and run cabal
       # for some reason this doesn't work without update
       # even though it doesn't actually download anything
-      run: nix develop -Lv -c bash -c "cabal update; cabal v1-build"
+      run: nix develop -Lv -c bash -c "cabal update; cabal v1-build"

.readthedocs.yaml

@@ -11,4 +11,4 @@ sphinx:
 # Explicitly set the version of Python and its requirements
 python:
   install:
-    - requirements: docs/requirements.txt
+    - requirements: docs/requirements.txt

docs/source/features.md

@@ -32,7 +32,7 @@ Standard data type declarations have a simple equivalent in Agda.
 Agda:
 ```agda
 data Nat : Type where
-    Zero : Nat 
+    Zero : Nat
     Suc : Nat → Nat
 
 {-# COMPILE AGDA2HS Nat #-}
@@ -52,7 +52,7 @@ Agda:
 data Tree (a : Type) : Type where
     Leaf   : a → Tree a
     Branch : a → Tree a → Tree a → Tree a
-    
+
 {-# COMPILE AGDA2HS Tree #-}
 ```
 
@@ -197,7 +197,7 @@ negate True = False
 negate False = True
 
 negate' :: Bool -> Bool
-negate' x = case x of 
+negate' x = case x of
     True -> False
     False -> True
 
@@ -260,7 +260,7 @@ createRange low high = if low <= high then Just (MkRange low high) else Nothing
 {-# COMPILE AGDA2HS createRange #-}
 
 createRangeCase : Int → Int → Maybe Range
-createRangeCase low high = 
+createRangeCase low high =
     case low <= high of λ where
         True → Just (MkRange low high)
         False → Nothing
@@ -393,7 +393,7 @@ open Equal public
 {-# COMPILE AGDA2HS Equal newtype #-}
 
 constructEqual : ⦃ iEqA : Eq a ⦄ → @0 ⦃ IsLawfulEq a ⦄ → (c : a) → (d : a) → Maybe (Equal a)
-constructEqual a b = 
+constructEqual a b =
   if a == b then
     (λ ⦃ h ⦄ → Just (MkEqual (a , b) (equality a b h)))
   else Nothing
@@ -475,10 +475,10 @@ record Class2 (a : Type) : Type where
 Haskell:
 ```hs
 class Class1 a where
-    field1 :: a 
+    field1 :: a
 
 class Class1 a => Class2 a where
-    field2 :: a 
+    field2 :: a
 ```
 
 ### Default Typeclass Field Implementations
@@ -507,7 +507,7 @@ open Ord ⦃ ... ⦄
 
 {-# COMPILE AGDA2HS Ord class Ord₁ Ord₂ #-}
 
-instance 
+instance
     Ord₁-Bool : Ord₁ Bool
     Ord₁-Bool .Ord₁._<_ False b = b
     Ord₁-Bool .Ord₁._<_ True _ = False
@@ -701,7 +701,7 @@ add1 = 1 +_
 
 Haskell:
 ```hs
-add1 :: Nat -> Nat 
+add1 :: Nat -> Nat
 add1 = (1 +)
 ```
 
@@ -729,7 +729,7 @@ even (Suc n) = odd n
 
 odd :: Nat -> Bool
 odd Zero = False
-odd (Suc n) = even n 
+odd (Suc n) = even n
 ```
 
 ### Mutually Recursive Datatype and Function

docs/source/tutorials.md

@@ -26,7 +26,7 @@ private
     rewrite sym $ concatMap-++-distr (map (u ∘_) v) (((pure _∘_) <*> us) <*> v) (λ f → map f w)
       | sym $ map-<*>-recomp v w u
       | compositionList us v w
-    = refl 
+    = refl
 
   interchangeList : {a b : Type} → (u : List (a → b)) → (y : a)
     → (u <*> (pure y)) ≡ (pure (_$ y) <*> u)

lib/base/Haskell/Law/Applicative/List.agda

@@ -6,4 +6,4 @@ open import Haskell.Prim.Int using ( int64 )
 open import Haskell.Law.Def
 
 int64-injective : Injective int64
-int64-injective refl = refl 
+int64-injective refl = refl

lib/base/Haskell/Law/Int.agda

@@ -12,7 +12,7 @@ open import Haskell.Prim.Applicative
 --------------------------------------------------
 -- _∷_
 
-module _ {x y : a} {xs ys : List a} where  
+module _ {x y : a} {xs ys : List a} where
   ∷-injective-left : x ∷ xs ≡ y ∷ ys → x ≡ y
   ∷-injective-left refl = refl
 
@@ -40,14 +40,14 @@ map-∘ g f (x ∷ xs) = cong (_ ∷_) (map-∘ g f xs)
 
 map-concatMap : ∀ (f : a → b) (xs : List a) → (map f xs) ≡ concatMap (λ g → f g ∷ []) xs
 map-concatMap f [] = refl
-map-concatMap f (x ∷ xs) 
+map-concatMap f (x ∷ xs)
   rewrite map-concatMap f xs
   = refl
 
-map-<*>-recomp : {a b c : Type} → (xs : List (a → b)) → (ys : List a) → (u : (b → c))  
+map-<*>-recomp : {a b c : Type} → (xs : List (a → b)) → (ys : List a) → (u : (b → c))
   → ((map (u ∘_) xs) <*> ys) ≡ map u (xs <*> ys)
 map-<*>-recomp [] _ _  = refl
-map-<*>-recomp (x ∷ xs) ys u 
+map-<*>-recomp (x ∷ xs) ys u
   rewrite map-∘ u x ys
     | map-++ u (map x ys) (xs <*> ys)
     | map-<*>-recomp  xs ys u
@@ -102,7 +102,7 @@ lengthNat-++ (x ∷ xs) = cong suc (lengthNat-++ xs)
 ++-cancel-right []       []       eq = refl
 ++-cancel-right (x ∷ xs) []       eq = ++-identity-left-unique (x ∷ xs) (sym eq)
 ++-cancel-right []       (y ∷ ys) eq = sym $ ++-identity-left-unique (y ∷ ys) eq
-++-cancel-right (x ∷ xs) (y ∷ ys) eq 
+++-cancel-right (x ∷ xs) (y ∷ ys) eq
   rewrite ∷-injective-left eq = cong (y ∷_) $ ++-cancel-right xs ys (∷-injective-right eq)
 
 ++-conical-left : (xs ys : List a) → xs ++ ys ≡ [] → xs ≡ []
@@ -114,7 +114,7 @@ lengthNat-++ (x ∷ xs) = cong suc (lengthNat-++ xs)
 ∷-not-identity : ∀ x (xs ys : List a) → (x ∷ xs) ++ ys ≡ ys → ⊥
 ∷-not-identity x xs ys eq = []≠∷ x xs (sym $ ++-identity-left-unique (x ∷ xs) (sym eq))
 
-concatMap-++-distr : ∀ (xs ys : List a) (f : a → List b) → 
+concatMap-++-distr : ∀ (xs ys : List a) (f : a → List b) →
   ((concatMap f xs) ++ (concatMap f ys)) ≡ (concatMap f (xs ++ ys))
 concatMap-++-distr [] ys f = refl
 concatMap-++-distr (x ∷ xs) ys f
@@ -129,7 +129,7 @@ foldr-universal : ∀ (h : List a → b) f e → (h [] ≡ e) →
                   (∀ x xs → h (x ∷ xs) ≡ f x (h xs)) →
                   ∀ xs → h xs ≡ foldr f e xs
 foldr-universal h f e base step []       = base
-foldr-universal h f e base step (x ∷ xs) rewrite step x xs = cong (f x) (foldr-universal h f e base step xs) 
+foldr-universal h f e base step (x ∷ xs) rewrite step x xs = cong (f x) (foldr-universal h f e base step xs)
 
 foldr-cong : ∀ {f g : a → b → b} {d e : b} →
             (∀ x y → f x y ≡ g x y) → d ≡ e →

lib/base/Haskell/Law/List.agda

@@ -16,6 +16,6 @@ instance
   iLawfulMonoidMaybe .leftIdentity = λ { Nothing → refl; (Just _) → refl }
 
   iLawfulMonoidMaybe .concatenation [] = refl
-  iLawfulMonoidMaybe .concatenation (x ∷ xs) 
+  iLawfulMonoidMaybe .concatenation (x ∷ xs)
     rewrite (concatenation xs)
     = refl

lib/base/Haskell/Law/Monoid/Maybe.agda

@@ -290,7 +290,7 @@ instance
   iLawfulNumInteger .IsLawfulNum.+-idˡ x = addInteger-idˡ x
   iLawfulNumInteger .IsLawfulNum.+-idʳ x = addInteger-idʳ x
   iLawfulNumInteger .IsLawfulNum.neg-inv x = n-n≡0-Integer x
-  iLawfulNumInteger .IsLawfulNum.*-assoc = mulInteger-assoc 
+  iLawfulNumInteger .IsLawfulNum.*-assoc = mulInteger-assoc
   iLawfulNumInteger .IsLawfulNum.*-idˡ x = mulInteger-idˡ x
   iLawfulNumInteger .IsLawfulNum.*-idʳ x = mulInteger-idʳ x
   iLawfulNumInteger .IsLawfulNum.distributeˡ = mulInteger-distributeˡ-addInteger

lib/base/Haskell/Law/Num/Integer.agda

@@ -61,7 +61,7 @@ addWord-comm : Commutative addWord
 addWord-comm = map-comm addWord addNat w2n n2w (embedding +-wordsAsNats) addNat-comm
 
 addWord-assoc : Associative addWord
-addWord-assoc = map-assoc addWord addNat w2n n2w (embedding +-wordsAsNats) addNat-assoc 
+addWord-assoc = map-assoc addWord addNat w2n n2w (embedding +-wordsAsNats) addNat-assoc
 
 mulWord-comm : Commutative mulWord
 mulWord-comm = map-comm mulWord mulNat w2n n2w (embedding *-wordsAsNats) mulNat-comm