Yes, such types are supported in Clean/ATS/Mercury.<br><br>Thanks,<br>Dmytro<br><br><div class="gmail_quote">2012/10/13 Nils Anders Danielsson <span dir="ltr">&lt;<a href="mailto:nad@chalmers.se" target="_blank">nad@chalmers.se</a>&gt;</span><br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im">On 2012-10-12 20:51, Dmytro Starosud wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Could you tell me please whether there is anything to support unique types in Agda?<br>
</blockquote>
<br></div>
Do you mean uniqueness types?<span class="HOEnZb"><font color="#888888"><br>
<br>
-- <br>
/NAD<br>
</font></span></blockquote></div><br>