As with everything, you can just click on Decidable in the hyperlinked HTML documentation to find out where the declaration you want is. Then you could just import Relation.Binary.Core and use Decidable from there. The fact that Relation.Binary re-exports it is a bit confusing, but doesn't really affect the procedure you'd normally use to import the symbol.<div>
<br></div><div>It's the same with GHC's Haskell though. A lot of core data/function declarations are made in the GHC.* namespace and then re-exported through their more familiar Data. counterparts. Haddock relieves some of the confusion in Haskell, but our HTML source performs a similar (almost better) task for finding things (if you know of one occurrence).</div>
<div class="gmail_extra"><br><br><div class="gmail_quote">On Fri, Nov 9, 2012 at 9:28 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 09:07:36AM -0500, Daniel Peebles wrote:<br>
> It's in Relation.Binary.Core, which is imported and then opened publicly at<br>
> the top of the file.<br>
><br>
<br>
</div> module Relation.Binary where<br>
...<br>
open import Relation.Binary.Core as Core using (_\equiv_)<br>
import Relation.Binary.Indexed.Core as I<br>
<br>
----------------------------------------------------------------------<br>
-- Simple properties and equivalence relations<br>
<br>
open Core public hiding (_\equiv_; refl; ...)<br>
...<br>
<br>
<br>
This combination of Core using (_\equiv_)<br>
and open Core public hiding (_\equiv_; refl; ...)<br>
is some feature!<br>
(difficult to understand).<br>
<br>
It is sometimes very difficult to find out from where to import a library<br>
thing.<br>
I do not know, may be import in lib can be set in a more plain way.<br>
<br>
Thanks,<br>
<br>
------<br>
Sergei<br>
</blockquote></div><br></div>