Merge pull request idris-lang#2495 from BlackBrane/master

Remove spurious Data.Fin imports (now reexported by Vect)
david-christiansen · Aug 6, 2015 · 030da05 · 030da05
2 parents 6784f7a + afe9481
commit 030da05
Show file tree

Hide file tree

Showing 3 changed files with 1 addition and 3 deletions.
diff --git a/libs/base/Data/HVect.idr b/libs/base/Data/HVect.idr
@@ -1,6 +1,5 @@
 module Data.HVect
 
-import Data.Fin
 import public Data.Vect
 
 %access public

diff --git a/libs/contrib/Control/Algebra.idr b/libs/contrib/Control/Algebra.idr
@@ -116,7 +116,7 @@ class RingWithUnity a => Field a where
   inverseM : (x : a) -> Not (x = neutral) -> a
 
 sum' : (Foldable t, Monoid a) => t a -> a
-sum' = foldr (<+>) neutral
+sum' = concat
 
 product' : (Foldable t, RingWithUnity a) => t a -> a
 product' = foldr (<.>) unity

diff --git a/libs/effects/Effect/Random.idr b/libs/effects/Effect/Random.idr
@@ -2,7 +2,6 @@ module Effect.Random
 
 import Effects
 import Data.Vect
-import Data.Fin
 
 data Random : Effect where 
      getRandom : sig Random Integer Integer