Libraries.Data.List.Extra

Reexports

Definitions

elemAt : List a -> Nat -> Maybe a

  Fetches the element at a given position.
  Returns `Nothing` if the position beyond the list's end.

Totality: total
Visibility: public export

findBy : (a -> Maybe b) -> List a -> Maybe b

Totality: total
Visibility: export

findBy' : (a -> Bool) -> List a -> (List a, (Maybe a, List a))

Totality: total
Visibility: export

findAndDeleteBy : (a -> Bool) -> List a -> Maybe (a, List a)

  Returns first element that matches the predicate and the list without it

Totality: total
Visibility: export

diffBy : (a -> a -> Bool) -> List a -> List a -> List a

  Compute the difference of two lists by the given predicate.
  Lists are treated as bags.

Totality: total
Visibility: export

dedup : Eq a => List a -> List a

  Remove adjacent duplicates

Totality: total
Visibility: export

sortedNub : Ord a => List a -> List a

  O(n * log(n)). Sort a list and remove duplicates

Totality: total
Visibility: export

lengthDistributesOverAppend : (xs : List a) -> (ys : List a) -> length (xs ++ ys) = length xs + length ys

  `List.length` is distributive over appending

Totality: total
Visibility: export