idris-0.10.1: test/idrisdoc003/TestDatatypes.idr
module TestDatatypes ||| This is another test public export data Test : Type where ||| Test constructor ATest : Test
module TestDatatypes ||| This is another test public export data Test : Type where ||| Test constructor ATest : Test