Idris-dev/test/reg040/expected