Skip to content

Commit 1e9b762

Browse files
committed
Back to Maybe.map
1 parent e5bed9f commit 1e9b762

File tree

2 files changed

+29
-1
lines changed

2 files changed

+29
-1
lines changed

src/Data/List/Base.agda

+1-1
Original file line numberDiff line numberDiff line change
@@ -404,7 +404,7 @@ findIndexᵇ : (A → Bool) → (x : List A) → Maybe $ Fin (length x)
404404
findIndexᵇ p [] = nothing
405405
findIndexᵇ p (x ∷ xs) = if p x
406406
then just zero
407-
else mapMaybe suc (findIndexᵇ p xs)
407+
else Maybe.map suc (findIndexᵇ p xs)
408408

409409
findIndicesᵇ : (A Bool) List A List ℕ
410410
findIndicesᵇ {A = A} p = h 0 where
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Function setoids and related constructions
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --cubical-compatible --safe #-}
8+
9+
module Function.Indexed.Relation.Binary.Equality where
10+
11+
open import Relation.Binary using (Setoid)
12+
open import Relation.Binary.Indexed.Heterogeneous using (IndexedSetoid)
13+
14+
-- A variant of setoid which uses the propositional equality setoid
15+
-- for the domain, and a more convenient definition of _≈_.
16+
17+
-- indexed
18+
≡-setoid : {f t₁ t₂} (From : Set f) IndexedSetoid From t₁ t₂ Setoid _ _
19+
≡-setoid From To = record
20+
{ Carrier = (x : From) Carrier x
21+
; _≈_ = λ f g x f x ≈ g x
22+
; isEquivalence = record
23+
{ refl = λ {f} x refl
24+
; sym = λ f∼g x sym (f∼g x)
25+
; trans = λ f∼g g∼h x trans (f∼g x) (g∼h x)
26+
}
27+
} where open IndexedSetoid To
28+

0 commit comments

Comments
 (0)