@@ -126,6 +126,20 @@ pow' : RingWithUnity a => a -> Nat -> a
126126pow' _ Z = unity
127127pow' x (S n) = x <.> pow' x n
128128
129+-- TODO: This can be more efficient:
130+-- stimes 5 x = x <+> (x <+> (x <+> (x <+> x)))
131+-- = x <+> ((x <+> x) <+> (x <+> x))
132+-- = let y = x <+> x in x <+> (y <+> y)
133+-- 4 <+>s into 3 <+>
134+||| Combine `n` copies of a value with `<+>`
135+stimes : Semigroup a => (n : Nat) -> {auto prf : IsSucc n} -> a -> a
136+stimes (S Z) x = x
137+stimes (S (S k)) x = x <+> stimes (S k) x
138+
139+||| Like `stimes`, but accepting `Z` as argument.
140+mtimes : Monoid a => (n : Nat) -> a -> a
141+mtimes Z x = neutral
142+mtimes (S k) x = stimes (S k) x
129143
130144-- XXX todo:
131145-- Structures where "abs" make sense.