module S08 (
  -- * Exercise 6
  -- | See <../pdfs/08.pdf>.

  -- * Exercise 3
  range',
  -- * Exercise 4
  prop_range_append,
  -- * Exercise 5
  splitAt'
  ) where
import Test.LeanCheck

range' = rng []
  where
    rng acc m n | m > n     = acc
                | otherwise = rng (n:acc) m (n-1)

splitAt' :: Int -> [a] -> ([a], [a])
splitAt' i xs | i <= 0 = ([], xs)
splitAt' i []          = ([], [])
splitAt' i (x:xs)      = (x:ys, zs)
  where (ys, zs) = splitAt' (i-1) xs

range m n
  | m > n = []
  | otherwise = m : range (m + 1) n

prop_range_append :: Int -> Int -> Bool
prop_range_append m n =
  m <= n ==> range m (n - 1) ++ [n] == range m n