idris-0.9.13: test/idrisdoc007/A.idr

module A

||| This is a test
data Test : Type where
  ||| Test constructor
  ATest : Test