idris-0.9.17: test/quasiquote005/expected