idris-0.9.9: test/test001/expected

24
12