[Agda] Decidable _\~~_ of Semiring

[Daniel Peebles]

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.

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).


On Fri, Nov 9, 2012 at 9:28 AM, Serge D. Mechveliani <mechvel at botik.ru>wrote:

> On Fri, Nov 09, 2012 at 09:07:36AM -0500, Daniel Peebles wrote:
> > It's in Relation.Binary.Core, which is imported and then opened publicly
> at
> > the top of the file.
> >
>
>   module Relation.Binary where
>   ...
>   open import Relation.Binary.Core as Core using (_\equiv_)
>   import Relation.Binary.Indexed.Core as I
>
>   ----------------------------------------------------------------------
>   -- Simple properties and equivalence relations
>
>   open Core public hiding (_\equiv_; refl; ...)
>   ...
>
>
> This combination of  Core using (_\equiv_)
> and                  open Core public hiding (_\equiv_; refl; ...)
> is some feature!
> (difficult to understand).
>
> It is sometimes very difficult to find out from where to import a library
> thing.
> I do not know, may be import in  lib  can be set in a more plain way.
>
> Thanks,
>
> ------
> Sergei
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20121109/fc8121c2/attachment.html