diff --git a/libs/base/Data/HVect.idr b/libs/base/Data/HVect.idr index b6e8badd28..acccb9c65a 100644 --- 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 index afde92318e..23335ee02b 100644 --- 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 index b10c91f727..55a08fc1d7 100644 --- 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