PLFA agda exercises
random_values