[Agda] Decidable _\~~_ of Semiring

[Daniel Peebles]

It's in Relation.Binary.Core, which is imported and then opened publicly at
the top of the file.


On Fri, Nov 9, 2012 at 8:57 AM, Serge D. Mechveliani <mechvel at botik.ru>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?
>
> Thanks,
>
> ------
> Sergei
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20121109/d08fbe7f/attachment.html