Idris2/tests/base/data_vect001/input