New upstream version 0.17

1 files changed, 28 insertions, 0 deletions

diff --git a/src/Data/List/Relation/Subset/Setoid.agda b/src/Data/List/Relation/Subset/Setoid.agda
new file mode 100644
index 0000000..86ef526
--- /dev/null
+++ b/src/Data/List/Relation/Subset/Setoid.agda
@@ -0,0 +1,28 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- The extensional sublist relation over setoid equality.
+------------------------------------------------------------------------
+
+open import Relation.Binary
+
+module Data.List.Relation.Subset.Setoid
+  {c ℓ} (S : Setoid c ℓ) where
+
+open import Data.List using (List)
+open import Data.List.Membership.Setoid S using (_∈_)
+open import Level using (_⊔_)
+open import Relation.Nullary using (¬_)
+
+open Setoid S renaming (Carrier to A)
+
+------------------------------------------------------------------------
+-- Definitions
+
+infix 4 _⊆_ _⊈_
+
+_⊆_ : Rel (List A) (c ⊔ ℓ)
+xs ⊆ ys = ∀ {x} → x ∈ xs → x ∈ ys
+
+_⊈_ : Rel (List A) (c ⊔ ℓ)
+xs ⊈ ys = ¬ xs ⊆ ys