git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2495 from BlackBrane/master
030da05Niklas Larsson
libs/base/Data/HVect.idr−1
compare with master
unifiedsplit
@@ -1,6 +1,5 @@
1module Data.HVect
1module Data.HVect
2
2
3−import Data.Fin
4import public Data.Vect
3import public Data.Vect
5
4
6%access public
5%access public
libs/contrib/Control/Algebra.idr+1−1
@@ -116,7 +116,7 @@ class RingWithUnity a => Field a where
116 inverseM : (x : a) -> Not (x = neutral) -> a
116 inverseM : (x : a) -> Not (x = neutral) -> a
117
117
118sum' : (Foldable t, Monoid a) => t a -> a
118sum' : (Foldable t, Monoid a) => t a -> a
119−sum' = foldr (<+>) neutral
119+sum' = concat
120
120
121product' : (Foldable t, RingWithUnity a) => t a -> a
121product' : (Foldable t, RingWithUnity a) => t a -> a
122product' = foldr (<.>) unity
122product' = foldr (<.>) unity
libs/effects/Effect/Random.idr−1
@@ -2,7 +2,6 @@ module Effect.Random
2
2
3import Effects
3import Effects
4import Data.Vect
4import Data.Vect
5−import Data.Fin
6
5
7data Random : Effect where
6data Random : Effect where
8 getRandom : sig Random Integer Integer
7 getRandom : sig Random Integer Integer