Skip to content

Commit 7239662

Browse files
committed
Fix tests
1 parent 9066b4d commit 7239662

File tree

4 files changed

+4
-5
lines changed

4 files changed

+4
-5
lines changed

src/Data/List/Base.agda

+1-2
Original file line numberDiff line numberDiff line change
@@ -346,8 +346,7 @@ findIndices {A = A} p = h 0 where
346346
h n [] = []
347347
h n (x ∷ xs) = if p x
348348
then n ∷ h (suc n) xs
349-
else h (suc n) xs
350-
349+
else h (suc n) xs
351350

352351
-- The following are functions which split a list up using boolean
353352
-- predicates. However, in practice they are difficult to use and

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ module Data.List.Membership.Setoid.Properties where
1111
open import Algebra using (Op₂; Selective)
1212
open import Data.Bool.Base using (true; false)
1313
open import Data.Fin.Base using (Fin; zero; suc)
14-
open import Data.List.Base
14+
open import Data.List.Base hiding (find)
1515
open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
1616
open import Data.List.Relation.Unary.All as All using (All)
1717
import Data.List.Relation.Unary.Any.Properties as Any

src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda

+1-1
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@
99
module Data.List.Relation.Binary.Subset.Setoid.Properties where
1010

1111
open import Data.Bool.Base using (Bool; true; false)
12-
open import Data.List.Base hiding (_∷ʳ_)
12+
open import Data.List.Base hiding (_∷ʳ_; find)
1313
open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
1414
open import Data.List.Relation.Unary.All as All using (All)
1515
import Data.List.Membership.Setoid as Membership

src/Data/List/Relation/Unary/Any/Properties.agda

+1-1
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ open import Data.Bool.Base using (Bool; false; true; T)
1212
open import Data.Bool.Properties using (T-∨; T-≡)
1313
open import Data.Empty using (⊥)
1414
open import Data.Fin.Base using (Fin; zero; suc)
15-
open import Data.List.Base as List
15+
open import Data.List.Base as List hiding (find)
1616
open import Data.List.Properties using (ʳ++-defn)
1717
open import Data.List.Effectful as Listₑ using (monad)
1818
open import Data.List.Relation.Unary.Any as Any using (Any; here; there)

0 commit comments

Comments
 (0)