Data.List.Ex

Reexports

Definitions

notTrivPairs : List a -> LazyList (a, a)

Totality: total
Visibility: public export

findDiffPairWhich : (a -> a -> Bool) -> List a -> LazyList (a, a)

Totality: total
Visibility: public export

findConsequentsWhich : (a -> a -> Bool) -> List a -> LazyList (a, a)

Totality: total
Visibility: public export

infixOf : Eq a => List a -> List a -> Maybe (List a, List a)

Totality: total
Visibility: public export

toNatList : Foldable f => f (Fin n) -> List Nat

Totality: total
Visibility: public export

mapI : (xs : List a) -> (Fin (xs .length) -> a -> b) -> List b

Totality: total
Visibility: public export

mapMaybeI : (xs : List a) -> (Fin (xs .length) -> a -> Maybe b) -> List b

Totality: total
Visibility: public export

filterI : (xs : List a) -> (Fin (xs .length) -> a -> Bool) -> List a

Totality: total
Visibility: public export

withIndex : (xs : List a) -> List (Fin (xs .length), a)

Totality: total
Visibility: public export

drop' : (xs : List a) -> Fin (S (xs .length)) -> List a

Totality: total
Visibility: public export

inits' : (xs : List a) -> DVect (xs .length) (\idx => Vect (S (finToNat idx)) a)

Totality: total
Visibility: export

findLastIndex : (a -> Bool) -> (xs : List a) -> Maybe (Fin (xs .length))

Totality: total
Visibility: export

zipV : (xs : List a) -> Vect (xs .length) b -> List (a, b)

Totality: total
Visibility: export
Fixity Declaration: infixr operator, level 6

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

Totality: total
Visibility: export