Idris2/tests/refc/refc001/expected