diff --git a/libs/base/Data/Vect.idr b/libs/base/Data/Vect.idr index ad8678bfc..83aa573b7 100644 --- a/libs/base/Data/Vect.idr +++ b/libs/base/Data/Vect.idr @@ -866,6 +866,18 @@ implementation Traversable (Vect k) where traverse f [] = pure [] traverse f (x :: xs) = [| f x :: traverse f xs |] +-------------------------------------------------------------------------------- +-- Semigroup/Monoid +-------------------------------------------------------------------------------- + +public export +Semigroup a => Semigroup (Vect k a) where + (<+>) = zipWith (<+>) + +public export +{k : Nat} -> Monoid a => Monoid (Vect k a) where + neutral = replicate k neutral + -------------------------------------------------------------------------------- -- Show --------------------------------------------------------------------------------