<div dir="ltr">I'm pretty sure it shouldn't be possible to do that in Idris (if it is, it's probably a bug), and I don't think most people want it in Agda either. The main reason it's undesriable is that it violates parametricity, which is a property most FP people really want.</div>
<div class="gmail_extra"><br><br><div class="gmail_quote">On Mon, Jan 21, 2013 at 12:58 PM, Dmytro Starosud <span dir="ltr"><<a href="mailto:d.starosud@gmail.com" target="_blank">d.starosud@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hello guys,<br><br>In Idris one can write:<br><pre>g : Type -> Bool
g Int = True
g _ = False</pre>Is it possible to do the same in Agda, in particular:<br><pre>type-dec : (A B : Set) -> Dec (A \equiv B)<br>type-dec = ?<br></pre>Thanks in advance!<br>
<br>_______________________________________________<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>