
  0 | module Data.List.TR
  1 | 
  2 | import Data.Iterable
  3 | import Data.List
  4 | import Control.MonadRec
  5 | import Control.Monad.Identity
  6 | 
  7 | export
  8 | replicateM : MonadRec m => Nat -> m a -> m (List a)
  9 | replicateM n ma = iterM (\_,as => (:: as) <$> ma) id Nil n
 10 | 
 11 | export
 12 | replicateTR : Nat -> a -> List a
 13 | replicateTR n va = run Nil n
 14 | 
 15 |   where
 16 |     run : List a -> Nat -> List a
 17 |     run xs 0     = xs
 18 |     run xs (S k) = run (va :: xs) k
 19 | 
 20 | export
 21 | iterateTR : Nat -> (a -> a) -> a -> List a
 22 | iterateTR n f = run Nil n
 23 | 
 24 |   where
 25 |     run : List a -> Nat -> a -> List a
 26 |     run xs 0     _  = reverse xs
 27 |     run xs (S k) va = run (va :: xs) k (f va)
 28 |