[Agda] decidable _∈_

[Sergei Meshveliani]

1. I am sorry for double-posting my previous letter 
   (caused due to the failure which reasons are not clear to me).

2. _∈?_ needs an additional argument.

For example,  Any.Membership  to include

  _∈?_ : {_≟_ : Decidable _≈_} → Decidable _∈_
  _∈?_ {_≟_} x =  any (_≟_ x)

So, the usage becomes like this:

  _∈'?_ = Membership._∈?_ {_≟'_}

  f x =  case  x ∈'? y  of ...

And now I doubt abut my suggestion.
Because  `any'  can be set directly in  _∈'?_ = ...

------
Sergei


On Thu, 2013-12-05 at 15:28 +0400, Sergei Meshveliani wrote:
> People,
> I write
>          _∈?_ x =  Data.List.Any.any (_≟_ x)
> 
> for the decidable list membership.
> But may be Standard library needs to have this   
>                                   _∈_ : (x : A) → Decidable (_∈_ x)
> ?
> 
> Thanks,
> 
> ------
> Sergei
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>