Operations using indexes #
Applies a function to each element of the list along with the index at which that element is found, returning the list of results. In addition to the index, the function is also provided with a proof that the index is valid.
List.mapIdx
is a variant that does not provide the function with evidence that the index is valid.
Equations
Instances For
Applies a function to each element of the list along with the index at which that element is found, returning the list of results.
List.mapFinIdx
is a variant that additionally provides the function with a proof that the index
is valid.
Equations
Instances For
Applies a monadic function to each element of the list along with the index at which that element is found, returning the list of results. In addition to the index, the function is also provided with a proof that the index is valid.
List.mapIdxM
is a variant that does not provide the function with evidence that the index is
valid.
Equations
Instances For
Auxiliary for mapFinIdxM
:
mapFinIdxM.go [a₀, a₁, ...] acc = acc.toList ++ [f 0 a₀ ⋯, f 1 a₁ ⋯, ...]
Equations
Instances For
Applies a monadic function to each element of the list along with the index at which that element is found, returning the list of results.
List.mapFinIdxM
is a variant that additionally provides the function with a proof that the index
is valid.