edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-11-27 10:41:08 +03:00
Code Issues Projects Releases Wiki Activity

Add find function to Data.List

Browse Source
This commit is contained in:
Niklas Larsson 2020-06-11 11:47:33 +02:00 committed by G. Allais
parent e9611b4ee1
commit 8fc166acd4
1 changed files with 6 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
libs/base/Data/List.idr
View File

@ -56,6 +56,12 @@ filter p (x :: xs)
then x :: filter p xs
else filter p xs
||| Find the first element of the list that satisfies the predicate.
public export
find : (p : a -> Bool) -> (xs : List a) -> Maybe a
find p [] = Nothing
find p (x::xs) = if p x then Just x else find p xs
||| Find associated information in a list using a custom comparison.
public export
lookupBy : (a -> a -> Bool) -> a -> List (a, b) -> Maybe b