[Agda] Exports example? Making ADT constructors private?

[Evan Czaplicki]

How would I make the Up constructor private in the following module? (Just
Up, but not Down)

module Movement where

data Direction where
    Up : Direction
    Down : Direction

I know there is a "private" annotation, but I'm not sure where to put it
for ADTs. Also, is "private" the primary way to mark what gets exported and
what does not? (i.e. is the Haskell way of doing things totally done away
with?)

Thank you!
Evan
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20131005/160776cd/attachment.html