diff --git a/CHANGELOG.md b/CHANGELOG.md index 89e22ce60e..b4b91488f7 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -33,6 +33,9 @@ Bug-fixes in `Function.Construct.Composition` had their arguments in the wrong order. They have been flipped so they can actually be used as a composition operator. +* The operations `_∷=_` and `_─_` exported from `Data.List.Membership.Setoid` + had an extraneous `{A : Set a}` parameter. This has been removed. + * The combinators `_≃⟨_⟩_` and `_≃˘⟨_⟩_` in `Data.Rational.Properties.≤-Reasoning` now correctly accepts proofs of type `_≃_` instead of the previous proofs of type `_≡_`. diff --git a/src/Data/List/Membership/Setoid.agda b/src/Data/List/Membership/Setoid.agda index 1b8a67fb7d..1a19169992 100644 --- a/src/Data/List/Membership/Setoid.agda +++ b/src/Data/List/Membership/Setoid.agda @@ -13,7 +13,7 @@ module Data.List.Membership.Setoid {c ℓ} (S : Setoid c ℓ) where open import Function.Base using (_∘_; id; flip) open import Data.List.Base as List using (List; []; _∷_; length; lookup) -open import Data.List.Relation.Unary.Any +open import Data.List.Relation.Unary.Any as Any using (Any; index; map; here; there) open import Data.Product.Base as Prod using (∃; _×_; _,_) open import Relation.Unary using (Pred) @@ -35,7 +35,8 @@ x ∉ xs = ¬ x ∈ xs ------------------------------------------------------------------------ -- Operations -open Data.List.Relation.Unary.Any using (_∷=_; _─_) public +_∷=_ = Any._∷=_ {A = A} +_─_ = Any._─_ {A = A} mapWith∈ : ∀ {b} {B : Set b} (xs : List A) → (∀ {x} → x ∈ xs → B) → List B