[Agda] Type decidability

[Daniel Peebles]

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.


On Mon, Jan 21, 2013 at 12:58 PM, Dmytro Starosud <d.starosud at gmail.com>wrote:

> Hello guys,
>
> In Idris one can write:
>
> g : Type -> Bool
> g Int = True
> g _ = False
>
> Is it possible to do the same in Agda, in particular:
>
> type-dec : (A B : Set) -> Dec (A \equiv B)
> type-dec = ?
>
> Thanks in advance!
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130121/aadbc128/attachment.html