[ add ] Data.List.Fresh.Membership.DecSetoid

CHANGELOG.md

@@ -100,6 +100,8 @@ New modules
 
 * `Algebra.Properties.Semiring`.
 
+* `Data.List.Fresh.Membership.DecSetoid`.
+
 * `Data.List.Relation.Binary.Permutation.Algorithmic{.Properties}` for the Choudhury and Fiore definition of permutation, and its equivalence with `Declarative` below.
 
 * `Data.List.Relation.Binary.Permutation.Declarative{.Properties}` for the least congruence on `List` making `_++_` commutative, and its equivalence with the `Setoid` definition.

src/Data/List/Fresh/Membership/DecSetoid.agda

@@ -0,0 +1,40 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Decidable setoid membership over fresh lists
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Relation.Binary.Bundles using (DecSetoid)
+
+module Data.List.Fresh.Membership.DecSetoid {a ℓ} (DS : DecSetoid a ℓ) where
+
+open import Level using (Level)
+open import Data.List.Fresh.Relation.Unary.Any using (any?)
+import Data.List.Fresh.Membership.Setoid as MembershipSetoid
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Definitions using (Decidable)
+open import Relation.Nullary.Decidable using (¬?)
+
+open DecSetoid DS using (setoid; _≟_) renaming (Carrier to A)
+
+private
+  variable
+    r : Level
+    R : Rel A r
+
+
+------------------------------------------------------------------------
+-- Re-export contents of Setoid membership
+open MembershipSetoid setoid public
+
+------------------------------------------------------------------------
+-- Other operations
+infix 4 _∈?_ _∉?_
+
+_∈?_ : Decidable (_∈_ {R = R})
+x ∈? xs = any? (x ≟_) xs
+
+_∉?_ : Decidable (_∉_ {R = R})
+x ∉? xs = ¬? (x ∈? xs)