Agda-stdlib: `elem` function for lists of types with decidable equality

[langston-barrett]

It looks to me like Data.List is missing a function elem, which in Haskell has type signature elem :: Eq a => a -> [a] -> Bool. Is this something that would be accepted if I wrote a version? Can someone point me to the corresponding interface for decidable equality (is it IsDecEquivalence in Relation.Binary )?

[gallais]

I suppose so. By the way, you can derive elem by combining:

any : ∀ {p} {P : A → Set p} → Decidable P → Decidable (Any P)
find : ∀ {p} {P : A → Set p} {xs} → Any P xs → ∃ λ x → x ∈ xs × P x
∃∈-Any : ∀ {a p} {A : Set a} {P : A → Set p} {xs} → (∃ λ x → x ∈ xs × P x) → Any P xs
map : ∀ {p q} {P : Set p} {Q : Set q} → P ⇔ Q → Dec P → Dec Q

[MatthewDaggitt]

So the principled Agda way to do this would be to use the decidability of Data.List.Any.Membership. This gives not only whether or not an element is in the list, but unlike a bool, will also give a data type that points to it.

I'm surprised that I can't seem to locate it in the library at the moment. I'll have another look at some point when I have more time and if not then I'll add it in for the release at the end of the month.

[andreasabel]

https://github.com/agda/agda-stdlib/blob/de23244a73d6dab55715fd5a107a5de805c55764/src/Data/List/Any.agda#L38

It should be a simple instance of

Data.List.Any.any

On 24.01.2018 23:43, MatthewDaggitt wrote:

So the principled Agda way to do this would be to use the decidability
of |Data.List.Membership|. This gives not only whether or not an element
is in the list, but unlike a bool, will also give a data type that
points to it.

I'm surprised that I can't seem to locate in the library at the moment.
I'll have another look at some point when I have more time and if not
then I'll add it in for the release at the end of the month.

—
You are receiving this because you are subscribed to this thread.
Reply to this email directly, view it on GitHub
https://github.com/agda/agda-stdlib/issues/220#issuecomment-360299117,
or mute the thread
https://github.com/notifications/unsubscribe-auth/ABGgks50eGODHYKwDzeHG78F0vuYJgciks5tN7H7gaJpZM4Rrw71.

--
Andreas Abel <>< Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.[email protected]
http://www.cse.chalmers.se/~abela/

[MatthewDaggitt]

Yup, good spot @andreasabel. Threw me off as it had no question mark after it! We should probably add an alias to it in membership...

[mechvel]

I also had this question. In the DoCon-A library, I set

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

  ⊆? : Decidable₂ _≈_ → Decidable₂ _⊆_
  ...
  ```
in   
```module ListOverSetoid {α α= : Level} (A : Setoid α α=)

[mechvel]

I meant "in the module parameterized by a Setoid".

[MatthewDaggitt]

Closed with d9400f1