Ok, thanks!<br><br><div class="gmail_quote">2013/1/23 Dan Rosén <span dir="ltr"><<a href="mailto:danr@student.chalmers.se" target="_blank">danr@student.chalmers.se</a>></span><br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
A remark, if you want to have something like decidable equality on<br>
types, you could encode a universe. There is much literature about<br>
this, one good starting point could be Stevan Andjelkovic's Master's<br>
Thesis: <a href="http://publications.lib.chalmers.se/records/fulltext/146810.pdf" target="_blank">http://publications.lib.chalmers.se/records/fulltext/146810.pdf</a>,<br>
see chapter 3 and onwards.<br>
<br>
Best,<br>
Dan<br>
<div class="im HOEnZb"><br>
On Mon, Jan 21, 2013 at 8:01 PM, Daniel Peebles <<a href="mailto:pumpkingod@gmail.com">pumpkingod@gmail.com</a>> wrote:<br>
> I'm pretty sure it shouldn't be possible to do that in Idris (if it is, it's<br>
> probably a bug), and I don't think most people want it in Agda either. The<br>
> main reason it's undesriable is that it violates parametricity, which is a<br>
> property most FP people really want.<br>
><br>
><br>
> On Mon, Jan 21, 2013 at 12:58 PM, Dmytro Starosud <<a href="mailto:d.starosud@gmail.com">d.starosud@gmail.com</a>><br>
> wrote:<br>
>><br>
</div><div class="HOEnZb"><div class="h5">>> Hello guys,<br>
>><br>
>> In Idris one can write:<br>
>><br>
>> g : Type -> Bool<br>
>> g Int = True<br>
>> g _ = False<br>
>><br>
>> Is it possible to do the same in Agda, in particular:<br>
>><br>
>> type-dec : (A B : Set) -> Dec (A \equiv B)<br>
>> type-dec = ?<br>
>><br>
>> Thanks in advance!<br>
>><br>
</div></div><div class="HOEnZb"><div class="h5">>> _______________________________________________<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>
><br>
</div></div></blockquote></div><br>