Idris2/tests/base/system_errno/input