123456789101112131415161718192021222324252627282930313233-------------------------------------------------------------------------- The Agda standard library---- Decidable setoid membership over lists------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} open import Relation.Binary.Bundles using (DecSetoid) module Data.List.Membership.DecSetoid {a ℓ} (DS : DecSetoid a ℓ) where open import Data.List.Relation.Unary.Any using (any?)open import Relation.Binary.Definitions using (Decidable)open import Relation.Nullary.Decidable using (¬?) open DecSetoid DS -------------------------------------------------------------------------- Re-export contents of propositional membership open import Data.List.Membership.Setoid (DecSetoid.setoid DS) public -------------------------------------------------------------------------- Other operations infix 4 _∈?_ _∉?_ _∈?_ : Decidable _∈_x ∈? xs = any? (x ≟_) xs _∉?_ : Decidable _∉_x ∉? xs = ¬? (x ∈? xs)