[Agda] Explicit export

[Jesper Cockx]

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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180124/d19337b7/attachment.html>