idris-0.9.17: test/docs001/input

:doc C