It's in Relation.Binary.Core, which is imported and then opened publicly at the top of the file.<div class="gmail_extra"><br><br><div class="gmail_quote">On Fri, Nov 9, 2012 at 8:57 AM, Serge D. Mechveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im">On Fri, Nov 09, 2012 at 01:40:06PM +0100, Andreas Abel wrote:<br>
> There are two different definitions of Decidable:<br>
><br>
> 1) The one in Relation.Unary is for predicates (unary relations).<br>
> 2) The one in Relation.Binary is for binary relations.<br>
><br>
> Just import the right one and the type error goes away.<br>
</div>> [..]<br>
<br>
I do not see in Relation.Binary of lib-0.6 any declaration of the<br>
Decidable type. Neither `data' nor `record' nor as a function.<br>
<br>
On the other hand<br>
open import Relation.Binary using ( Decidable )<br>
does help<br>
-- !?<br>
How can this import work?<br>
<br>
Thanks,<br>
<div class="HOEnZb"><div class="h5"><br>
------<br>
Sergei<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>
</div></div></blockquote></div><br></div>