File tree Expand file tree Collapse file tree 1 file changed +12
-0
lines changed Expand file tree Collapse file tree 1 file changed +12
-0
lines changed Original file line number Diff line number Diff line change @@ -866,6 +866,18 @@ implementation Traversable (Vect k) where
866
866
traverse f [] = pure []
867
867
traverse f (x :: xs) = [| f x :: traverse f xs | ]
868
868
869
+ -- ------------------------------------------------------------------------------
870
+ -- Semigroup/Monoid
871
+ -- ------------------------------------------------------------------------------
872
+
873
+ public export
874
+ Semigroup a => Semigroup (Vect k a) where
875
+ (<+> ) = zipWith (<+> )
876
+
877
+ public export
878
+ {k : Nat } -> Monoid a => Monoid (Vect k a) where
879
+ neutral = replicate k neutral
880
+
869
881
-- ------------------------------------------------------------------------------
870
882
-- Show
871
883
-- ------------------------------------------------------------------------------
You can’t perform that action at this time.
0 commit comments