<div dir="ltr">Does Agda have an explicit export feature like in Haskell? As in e.g.:<div><br></div><div>    module That ( would ; be ; nice ; ! ) where</div><div><div><br></div>-- <br><div class="gmail_signature" data-smartmail="gmail_signature"><div>Regards</div><div><i>Frederik Hanghøj Iversen</i></div></div>
</div></div>