Merge tag 'upstream/0.17'

Upstream version 0.17

# gpg: Signature made Fri 23 Nov 2018 05:29:18 PM MST
# gpg:                using RSA key 9B917007AE030E36E4FC248B695B7AE4BF066240
# gpg:                issuer "spwhitton@spwhitton.name"
# gpg: Good signature from "Sean Whitton <spwhitton@spwhitton.name>" [ultimate]
# Primary key fingerprint: 8DC2 487E 51AB DD90 B5C4  753F 0F56 D055 3B6D 411B
#      Subkey fingerprint: 9B91 7007 AE03 0E36 E4FC  248B 695B 7AE4 BF06 6240

1 files changed, 59 insertions, 0 deletions

diff --git a/src/Data/List/Membership/Setoid.agda b/src/Data/List/Membership/Setoid.agda
new file mode 100644
index 0000000..a3384f1
--- /dev/null
+++ b/src/Data/List/Membership/Setoid.agda
@@ -0,0 +1,59 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- List membership and some related definitions
+------------------------------------------------------------------------
+
+open import Relation.Binary
+
+module Data.List.Membership.Setoid {c ℓ} (S : Setoid c ℓ) where
+
+open import Function using (_∘_; id; flip)
+open import Data.List.Base using (List; []; _∷_)
+open import Data.List.Any using (Any; map; here; there)
+open import Data.Product as Prod using (∃; _×_; _,_)
+open import Relation.Nullary using (¬_)
+
+open Setoid S renaming (Carrier to A)
+
+------------------------------------------------------------------------
+-- Definitions
+
+infix 4 _∈_ _∉_
+
+_∈_ : A → List A → Set _
+x ∈ xs = Any (x ≈_) xs
+
+_∉_ : A → List A → Set _
+x ∉ xs = ¬ x ∈ xs
+
+------------------------------------------------------------------------
+-- Operations
+
+mapWith∈ : ∀ {b} {B : Set b}
+           (xs : List A) → (∀ {x} → x ∈ xs → B) → List B
+mapWith∈ []       f = []
+mapWith∈ (x ∷ xs) f = f (here refl) ∷ mapWith∈ xs (f ∘ there)
+
+find : ∀ {p} {P : A → Set p} {xs} →
+       Any P xs → ∃ λ x → x ∈ xs × P x
+find (here px)   = (_ , here refl , px)
+find (there pxs) = Prod.map id (Prod.map there id) (find pxs)
+
+lose : ∀ {p} {P : A → Set p} {x xs} →
+       P Respects _≈_ → x ∈ xs → P x → Any P xs
+lose resp x∈xs px = map (flip resp px) x∈xs
+
+------------------------------------------------------------------------
+-- DEPRECATED
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 0.16
+
+map-with-∈ = mapWith∈
+{-# WARNING_ON_USAGE map-with-∈
+"Warning: map-with-∈ was deprecated in v0.16.
+Please use mapWith∈ instead."
+#-}