Idris2Doc : Data.List.Extra

Data.List.Extra

Definitions

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
Visibility: public export
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
Visibility: public export
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
Visibility: public export