[Agda] Exports example? Making ADT constructors private?
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
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Agda