------------------------------------------------------------------------ -- The Agda standard library -- -- The extensional sublist relation over setoid equality. ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} open import Relation.Binary.Core using (Rel) open import Relation.Binary.Bundles using (Setoid) module Data.List.Relation.Binary.Subset.Setoid {c ℓ} (S : Setoid c ℓ) where open import Data.List.Base using (List) open import Data.List.Membership.Setoid S using (_∈_) open import Function.Base using (flip) open import Level using (_⊔_) open import Relation.Nullary.Negation 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 ⊔ ℓ) _⊇_ = flip _⊆_ _⊈_ : Rel (List A) (c ⊔ ℓ) xs ⊈ ys = ¬ xs ⊆ ys _⊉_ : Rel (List A) (c ⊔ ℓ) xs ⊉ ys = ¬ xs ⊇ ys