Idris-dev/test/reg057/expected