[Agda] Type decidability
d.starosud at gmail.com
Wed Jan 23 13:37:31 CET 2013
I think, one can achieve some decidability using reflection.
2013/1/21 Daniel Peebles <pumpkingod at gmail.com>
> 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
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Agda