Agda2

From Rosetta Code