Idris2Doc : Data.List.Extra

Data.List.Extra

filterLoc : (a -> Bool) -> Lista -> (Lista, ListNat)
  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
filterLoc' : (a -> Bool) -> Lista -> 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
mapi : (Nat -> a -> b) -> Lista -> Listb
  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