Discussion:
Explicit export
(too old to reply)
Frederik Hanghøj Iversen
2018-01-24 15:36:08 UTC
Permalink
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*
Jesper Cockx
2018-01-24 15:45:00 UTC
Permalink
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 <
Post by Frederik Hanghøj Iversen
module That ( would ; be ; nice ; ! ) where
--
Regards
*Frederik HanghÞj Iversen*
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
Frederik Hanghøj Iversen
2018-01-24 15:55:26 UTC
Permalink
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.
Post by 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 <
Post by Frederik Hanghøj Iversen
module That ( would ; be ; nice ; ! ) where
--
Regards
*Frederik HanghÞj Iversen*
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
--
Regards
*Frederik HanghÞj Iversen*
Wolfram Kahl
2018-01-24 16:19:28 UTC
Permalink
Post by Frederik Hanghøj Iversen
On Wed, Jan 24, 2018 at 4:36 PM, Frederik Hanghøj Iversen <
Post by Frederik Hanghøj Iversen
module That ( would ; be ; nice ; ! ) where
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

Loading...