idris-0.9.12: test/tutorial003/expected