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