idris-0.9.17: test/tactics001/expected