[Agda] Explicit export

[Frederik Hanghøj Iversen]

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.

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'.
>
> -- Jesper
>
> 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
>>
>> --
>> Regards
>> *Frederik Hanghøj Iversen*
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>>
>


-- 
Regards
*Frederik Hanghøj Iversen*
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180124/0d5c2867/attachment.html>