idris-0.9.9: test/reg005/expected

1f4o1b4a1r1b3a1z