[Agda] Exports example? Making ADT constructors private?

[Nils Anders Danielsson]

On 2013-10-06 16:21, Brian McKenna wrote:
> 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'

An alternative method:

   module Movement where

   private

     module Dummy where

       data Direction : Set where
         Up Down : Direction

   open Dummy public hiding (Down)

-- 
/NAD