Data.List.Extra

Definitions

mapi : (Nat -> a -> b) -> List a -> List b

  Analogous to `map` for `List`, but the function is applied to the index of
  the element as first argument (counting from 0), and the element itself as
  second argument.

Totality: total
Visibility: public export

filterLoc : (a -> Bool) -> List a -> (List a, List Nat)

  Applied to a predicate and a list, returns the list of those elements that
  satisfy the predicate with corresponding indices in a stand-alone list.
  See also `Data.List.Extra.filterLoc'`.

Totality: total
Visibility: public export

filterLoc' : (a -> Bool) -> List a -> List (a, Nat)

  Applied to a predicate and a list, returns the list of those elements that
  satisfy the predicate with corresponding indices.

Totality: total
Visibility: public export