<div dir="ltr"><div>That makes sense, thank you :) Do you like doing things that way? Like, more than the big list at the top of the file?</div><div><br></div>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.</div>
<div class="gmail_extra"><br><br><div class="gmail_quote">On Sun, Oct 6, 2013 at 7:21 AM, Brian McKenna <span dir="ltr"><<a href="mailto:brian@brianmckenna.org" target="_blank">brian@brianmckenna.org</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Evan,<br>
<br>
Awesome to see you on the Agda list. I hope it'll influence Elm.<br>
<br>
The way I know how to do this is like so:<br>
<br>
module Movement where<br>
<br>
private<br>
data Direction' : Set0 where<br>
Up : Direction'<br>
Down : Direction'<br>
<br>
open Direction' public hiding (Down)<br>
<br>
Direction : Set0<br>
Direction = Direction'<br>
<br>
You can probably see what's happening with the private block and the<br>
open import. The interesting thing is that (as far as I can tell) the<br>
open import doesn't re-export the Direction' type, therefore we have<br>
to do that ourselves.<br>
<br>
Does that make sense?<br>
<br>
Thanks,<br>
Brian McKenna<br>
<div><div class="h5"><br>
On 5 October 2013 20:30, Evan Czaplicki <<a href="mailto:evancz@gmail.com">evancz@gmail.com</a>> wrote:<br>
> How would I make the Up constructor private in the following module? (Just<br>
> Up, but not Down)<br>
><br>
> module Movement where<br>
><br>
> data Direction where<br>
> Up : Direction<br>
> Down : Direction<br>
><br>
> I know there is a "private" annotation, but I'm not sure where to put it for<br>
> ADTs. Also, is "private" the primary way to mark what gets exported and what<br>
> does not? (i.e. is the Haskell way of doing things totally done away with?)<br>
><br>
> Thank you!<br>
> Evan<br>
><br>
</div></div>> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
><br>
</blockquote></div><br></div>