idris-learning/chapter2/average