idris-0.9.11: test/reg005/expected