<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&#39;ve had my eye on parameterized modules and implicit arguments for a while now, and I plan features knowing that I&#39;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">&lt;<a href="mailto:brian@brianmckenna.org" target="_blank">brian@brianmckenna.org</a>&gt;</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&#39;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&#39; : Set0 where<br>
           Up : Direction&#39;<br>
           Down : Direction&#39;<br>
<br>
    open Direction&#39; public hiding (Down)<br>
<br>
    Direction : Set0<br>
    Direction = Direction&#39;<br>
<br>
You can probably see what&#39;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&#39;t re-export the Direction&#39; 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 &lt;<a href="mailto:evancz@gmail.com">evancz@gmail.com</a>&gt; wrote:<br>
&gt; How would I make the Up constructor private in the following module? (Just<br>
&gt; Up, but not Down)<br>
&gt;<br>
&gt; module Movement where<br>
&gt;<br>
&gt; data Direction where<br>
&gt;     Up : Direction<br>
&gt;     Down : Direction<br>
&gt;<br>
&gt; I know there is a &quot;private&quot; annotation, but I&#39;m not sure where to put it for<br>
&gt; ADTs. Also, is &quot;private&quot; the primary way to mark what gets exported and what<br>
&gt; does not? (i.e. is the Haskell way of doing things totally done away with?)<br>
&gt;<br>
&gt; Thank you!<br>
&gt; Evan<br>
&gt;<br>
</div></div>&gt; _______________________________________________<br>
&gt; Agda mailing list<br>
&gt; <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
&gt; <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
&gt;<br>
</blockquote></div><br></div>