[Agda] Exports example? Making ADT constructors private?

Evan Czaplicki evancz at gmail.com
Sun Oct 6 04:30:46 CEST 2013

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

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

More information about the Agda mailing list