[Agda] Type decidability

[Dmytro Starosud]

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!
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130121/4b3c9b03/attachment.html