Andre Dublin (4) [Avatar] Offline
I would consider introducing the reader to zipWith, it took me a while to understand how to execute the function.

Also the doc for zipWith is a little confusing

Prelude.List.zipWith : (f : a -> b -> c) ->
    (l : List a) -> (r : List b) -> List c
    Combine two lists elementwise using some function. If they are
    different lengths, the result is truncated to the length of the
    shorter list.
        f : a -> b -> c  -- the function to combine elements with

        l : List a  -- the first list

        r : List b  -- the second list

    The function is Total

Prelude.Stream.zipWith : (a -> b -> c) ->
    Stream a -> Stream b -> Stream c
    Combine two streams element-wise using a function

    The function is Total

Data.Vect.zipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
    Combine two equal-length vectors pairwise with some function

    The function is Total

My problem with the documentation about is that Data.Vect.zipWith and Prelude.Stream.zipWith don't show a function in the definition signature as Prelude.List.zipWith does.