Merge pull request #2495 from BlackBrane/master
Remove spurious Data.Fin imports (now reexported by Vect)
commit030da056bc0faad98f5a97f1e921c0342f4dc3a3
authorNiklas Larsson <metaniklas@gmail.com>
dateThu 6 Aug 2015, 18:09 (11 years ago)
parent6784f7aafe9481
libs/base/Data/HVect.idr−1
@@ -1,6 +1,5 @@
11module Data.HVect
22
3−import Data.Fin
43import public Data.Vect
54
65%access public
libs/contrib/Control/Algebra.idr+1−1
@@ -116,7 +116,7 @@ class RingWithUnity a => Field a where
116116 inverseM : (x : a) -> Not (x = neutral) -> a
117117
118118sum' : (Foldable t, Monoid a) => t a -> a
119−sum' = foldr (<+>) neutral
119+sum' = concat
120120
121121product' : (Foldable t, RingWithUnity a) => t a -> a
122122product' = foldr (<.>) unity
libs/effects/Effect/Random.idr−1
@@ -2,7 +2,6 @@ module Effect.Random
22
33import Effects
44import Data.Vect
5−import Data.Fin
65
76data Random : Effect where
87 getRandom : sig Random Integer Integer