Skip to content

Commit b732929

Browse files
committedOct 17, 2023
[ fix agda#2153 ] Properly re-export specialised combinators
1 parent cc0172d commit b732929

File tree

1 file changed

+3
-2
lines changed

1 file changed

+3
-2
lines changed
 

‎src/Data/List/Membership/Setoid.agda

+3-2
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ module Data.List.Membership.Setoid {c ℓ} (S : Setoid c ℓ) where
1313

1414
open import Function.Base using (_∘_; id; flip)
1515
open import Data.List.Base as List using (List; []; _∷_; length; lookup)
16-
open import Data.List.Relation.Unary.Any
16+
open import Data.List.Relation.Unary.Any as Any
1717
using (Any; index; map; here; there)
1818
open import Data.Product.Base as Prod using (∃; _×_; _,_)
1919
open import Relation.Unary using (Pred)
@@ -35,7 +35,8 @@ x ∉ xs = ¬ x ∈ xs
3535
------------------------------------------------------------------------
3636
-- Operations
3737

38-
open Data.List.Relation.Unary.Any using (_∷=_; _─_) public
38+
_∷=_ = Any._∷=_ {A = A}
39+
_─_ = Any._─_ {A = A}
3940

4041
mapWith∈ : {b} {B : Set b}
4142
(xs : List A) ( {x} x ∈ xs B) List B

0 commit comments

Comments
 (0)