idris-0.9.19: test/syntax002/expected

Nothing
7