idris-0.9.17: test/docs002/input

:doc T1
:doc T2
:doc T3