[Agda] Exports example? Making ADT constructors private?

[Brian McKenna]

Hi Evan,

Awesome to see you on the Agda list. I hope it'll influence Elm.

The way I know how to do this is like so:

    module Movement where

    private
      data Direction' : Set0 where
           Up : Direction'
           Down : Direction'

    open Direction' public hiding (Down)

    Direction : Set0
    Direction = Direction'

You can probably see what's happening with the private block and the
open import. The interesting thing is that (as far as I can tell) the
open import doesn't re-export the Direction' type, therefore we have
to do that ourselves.

Does that make sense?

Thanks,
Brian McKenna

On 5 October 2013 20:30, Evan Czaplicki <evancz at gmail.com> wrote:
> 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
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>