[Agda] Decidable _\~~_ of Semiring

[Serge D. Mechveliani]

On Fri, Nov 09, 2012 at 05:57:19PM +0400, Serge D. Mechveliani wrote:
> On Fri, Nov 09, 2012 at 01:40:06PM +0100, Andreas Abel wrote:
> > There are two different definitions of Decidable:
> >
> > 1) The one in Relation.Unary is for predicates (unary relations).
> > 2) The one in Relation.Binary is for binary relations.
> >
> > Just import the right one and the type error goes away.
> > [..]
> 
> I do not see in  Relation.Binary  of lib-0.6  any declaration of the  
> Decidable  type. Neither `data' nor `record' nor as a function. 
> 
> On the other hand  
>                   open import Relation.Binary using ( Decidable )
> does help
> -- !?
> How can this import work? 

Relation.Binary  has 
             open import Relation.Binary.Core as Core using ( \equiv )
,
and  Relation.Binary.Core  does declare  Decidable.
But  " using ( \equiv ) "  hides everything in this import except  \equiv,
so  Decidable  is not imported to  Relation.Binary,  and cannot be imported
from it.
Right?

Thanks,

------
Sergei