idris-0.9.15: test/reg052/expected

000000000000002A