idris-0.12: test/regression001/expected