[Agda] Exports example? Making ADT constructors private?
evancz at gmail.com
Wed Oct 9 20:09:40 CEST 2013
That makes sense, thank you :) Do you like doing things that way? Like,
more than the big list at the top of the file?
P.S. Agda has already influenced Elm :) I've had my eye on parameterized
modules and implicit arguments for a while now, and I plan features knowing
that I'm probably adding these someday :) Also, I have not written tons of
Agda yet, but I am constantly impressed by how it gracefully it extends and
simplifies syntax and semantics.
On Sun, Oct 6, 2013 at 7:21 AM, Brian McKenna <brian at brianmckenna.org>wrote:
> Hi Evan,
> Awesome to see you on the Agda list. I hope it'll influence Elm.
> The way I know how to do this is like so:
> module Movement where
> data Direction' : Set0 where
> Up : Direction'
> Down : Direction'
> open Direction' public hiding (Down)
> Direction : Set0
> Direction = Direction'
> You can probably see what's happening with the private block and the
> open import. The interesting thing is that (as far as I can tell) the
> open import doesn't re-export the Direction' type, therefore we have
> to do that ourselves.
> Does that make sense?
> Brian McKenna
> On 5 October 2013 20:30, Evan Czaplicki <evancz at gmail.com> wrote:
> > How would I make the Up constructor private in the following module?
> > Up, but not Down)
> > module Movement where
> > data Direction where
> > Up : Direction
> > Down : Direction
> > I know there is a "private" annotation, but I'm not sure where to put it
> > ADTs. Also, is "private" the primary way to mark what gets exported and
> > does not? (i.e. is the Haskell way of doing things totally done away
> > Thank you!
> > Evan
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Agda