[Agda] Explicit export

[Wolfram Kahl]

On Wed, Jan 24, 2018 at 04:55:26PM +0100, Frederik Hanghøj Iversen wrote:
> > On Wed, Jan 24, 2018 at 4:36 PM, Frederik Hanghøj Iversen <
> > fhi.1990 at gmail.com> wrote:
> >
> >> Does Agda have an explicit export feature like in Haskell? As in e.g.:
> >>
> >>     module That ( would ; be ; nice ; ! ) where
>
> On Wed, Jan 24, 2018 at 4:45 PM, Jesper Cockx <Jesper at sikanda.be> wrote:
> 
> > Agda works a bit different from Haskell wrt the module system, but you can
> > use the 'private' keyword to prevent certain functions in a module from
> > being exported. If you want to re-export a definition from a different
> > module, you can use 'open M using (...) public'.
>
> Right... However, in most cases I find it preferable to be explicit about
> what you *put* in scope rather than what you *hide* from it.

You could write a wrapper module:

    module M where
    
      private module M0 where
        ... everything, including all the internal stuff
    
      open M0 public using (what ; you ; want ; to ; export )
    

Wolfram