From c9de4d9f9fa336b4bf6b6b68b18f7c536734d735 Mon Sep 17 00:00:00 2001
From: Edwin Brady <ecb10@st-andrews.ac.uk>
Date: Wed, 3 Mar 2021 14:36:33 +0000
Subject: [PATCH] Remove more trailing whitespace

---
 tests/idris2/interface024/EH.idr | 46 ++++++++++++++++----------------
 1 file changed, 23 insertions(+), 23 deletions(-)

diff --git a/tests/idris2/interface024/EH.idr b/tests/idris2/interface024/EH.idr
index edbb3ba92..348ad9948 100644
--- a/tests/idris2/interface024/EH.idr
+++ b/tests/idris2/interface024/EH.idr
@@ -12,20 +12,20 @@ interface Additive a where
 interface Additive2 a where
   constructor MkAdditive2
   (:+:) : a -> a -> a
-  O2   : a 
-  
+  O2   : a
+
 interface Multiplicative a where
   constructor MkMultiplicative
   (.*.) : a -> a -> a
   I     : a
 
-record MonoidOver U where            
+record MonoidOver U where
   constructor WithStruct
   Unit    : U
   Mult    : U -> U -> U
   lftUnit : (x : U) -> Unit `Mult` x    = x
   rgtUnit : (x : U) -> x    `Mult` Unit = x
-  assoc   : (x,y,z : U) 
+  assoc   : (x,y,z : U)
                     -> x `Mult` (y `Mult` z) = (x `Mult` y) `Mult` z
 
 record Monoid where
@@ -34,12 +34,12 @@ record Monoid where
   Struct : MonoidOver U
 
 AdditiveStruct : (m : MonoidOver a) -> Additive a
-AdditiveStruct m = MkAdditive (Mult $ m) 
+AdditiveStruct m = MkAdditive (Mult $ m)
                               (Unit $ m)
 AdditiveStruct2 : (m : MonoidOver a) -> Additive2 a
-AdditiveStruct2 m = MkAdditive2 (Mult $ m) 
+AdditiveStruct2 m = MkAdditive2 (Mult $ m)
                                 (Unit $ m)
-AdditiveStructs : (ma : MonoidOver a) -> (mb : MonoidOver b) 
+AdditiveStructs : (ma : MonoidOver a) -> (mb : MonoidOver b)
               -> (Additive a, Additive2 b)
 AdditiveStructs ma mb = (AdditiveStruct ma, AdditiveStruct2 mb)
 
@@ -49,46 +49,46 @@ getAdditive m = AdditiveStruct (Struct m)
 MultiplicativeStruct : (m : Monoid) -> Multiplicative (U m)
 MultiplicativeStruct m = MkMultiplicative (Mult $ Struct m)
                                           (Unit $ Struct m)
------------------------------------------------------                   
+-----------------------------------------------------
 
 Commutative : MonoidOver a -> Type
 Commutative m = (x,y : a) -> let _ = AdditiveStruct m in
                 x .+. y = y .+. x
-                
+
 Commute : (Additive a, Additive2 a) => Type
 Commute =
-          (x11,x12,x21,x22 : a) -> 
+          (x11,x12,x21,x22 : a) ->
           ((x11 :+: x12) .+. (x21 :+: x22))
           =
           ((x11 .+. x21) :+: (x12 .+. x22))
 
-product : (ma, mb : Monoid) -> Monoid 
-product ma mb = 
-  let 
+product : (ma, mb : Monoid) -> Monoid
+product ma mb =
+  let
       %hint aStruct : Additive (U ma)
       aStruct = getAdditive ma
       %hint bStruct : Additive (U mb)
       bStruct = getAdditive mb
-      
+
   in MkMonoid (U ma, U mb) $ WithStruct
      (O, O)
      (\(x1,y1), (x2, y2)  => (x1 .+. x2, y1 .+. y2))
-     (\(x,y) => rewrite lftUnit (Struct ma) x in 
+     (\(x,y) => rewrite lftUnit (Struct ma) x in
                 rewrite lftUnit (Struct mb) y in
                 Refl)
      (\(x,y) => rewrite rgtUnit (Struct ma) x in
                 rewrite rgtUnit (Struct mb) y in
                 Refl)
-     (\(x1,y1),(x2,y2),(x3,y3) => 
+     (\(x1,y1),(x2,y2),(x3,y3) =>
                 rewrite assoc (Struct ma) x1 x2 x3 in
                 rewrite assoc (Struct mb) y1 y2 y3 in
                 Refl)
 
-EckmannHilton : forall a . (ma,mb : MonoidOver a) 
+EckmannHilton : forall a . (ma,mb : MonoidOver a)
              -> let ops = AdditiveStructs ma mb in
                 Commute @{ops}
              -> (Commutative ma, (x,y : a) -> x .+. y = x :+: y)
-EckmannHilton ma mb prf = 
+EckmannHilton ma mb prf =
   let %hint first : Additive a
       first = AdditiveStruct ma
       %hint second : Additive2 a
@@ -97,7 +97,7 @@ EckmannHilton ma mb prf =
       SameUnits = Calc $
         |~ O
         ~~  O         .+.         O  ...(sym $ lftUnit ma O)
-        ~~ (O :+: O2) .+. (O2 :+: O) ...(sym $ cong2 (.+.) 
+        ~~ (O :+: O2) .+. (O2 :+: O) ...(sym $ cong2 (.+.)
                                              (rgtUnit mb O)
                                              (lftUnit mb O))
         ~~ (O .+. O2) :+: (O2 .+. O) ...(prf O O2 O2 O)
@@ -105,7 +105,7 @@ EckmannHilton ma mb prf =
                                              (lftUnit ma O2)
                                              (rgtUnit ma O2))
         ~~ O2                        ...(lftUnit mb O2)
-        
+
       SameMults : (x,y : a) -> (x .+. y) === (x :+: y)
       SameMults x y = Calc $
         |~ x .+. y
@@ -113,13 +113,13 @@ EckmannHilton ma mb prf =
                                              (rgtUnit mb x)
                                              (lftUnit mb y))
         ~~ (x .+. O2) :+: (O2 .+. y) ...(prf x O2 O2 y)
-        ~~ (x .+. O ) :+: (O  .+. y) ...(cong (\u => 
+        ~~ (x .+. O ) :+: (O  .+. y) ...(cong (\u =>
                                               (x .+. u) :+: (u .+. y))
                                               (sym SameUnits))
         ~~ x :+: y                   ...(cong2 (:+:)
                                               (rgtUnit ma x)
                                               (lftUnit ma y))
-                                                    
+
       Commutativity : Commutative ma
       Commutativity x y = Calc $
         |~ x .+. y
@@ -127,7 +127,7 @@ EckmannHilton ma mb prf =
                                              (lftUnit mb x)
                                              (rgtUnit mb y))
         ~~ (O2 .+. y) :+: (x .+. O2) ...(prf O2 x y O2)
-        ~~ (O  .+. y) :+: (x .+. O ) ...(cong (\u => 
+        ~~ (O  .+. y) :+: (x .+. O ) ...(cong (\u =>
                                               (u .+. y) :+: (x .+. u))
                                               (sym SameUnits))
         ~~ y :+: x                   ...(cong2 (:+:)