Spidr.Data.List

List definitions.

Reexports

Definitions

range : Nat -> List Nat

  All numbers from `0` to `n - 1` inclusive, in increasing order.
  
  @n The (exclusive) limit of the range.

Totality: total
Visibility: export

enumerate : List a -> List (Nat, a)

  Enumerate entries in a list with their indices. For example, `enumerate [5, 7, 9]`
  is `[(0, 5), (1, 7), (2, 9)]`.

Totality: total
Visibility: export

unique : Eq a => List a -> Bool

  `True` if there are no duplicate elements in the list, else `False`.
  
  This function has time complexity quadratic in the list length.

Totality: total
Visibility: public export

multiIndex : (idxs : List Nat) -> (xs : List a) -> {auto 0 _ : All (flip InBounds xs) idxs} -> List a

  Index multiple values from a list at once. For example,
  `multiIndex [1, 3] [5, 6, 7, 8]` is `[6, 8]`.
  
  @idxs The indices at which to index.
  @xs The list to index.

Totality: total
Visibility: public export

deleteAt : (idxs : List Nat) -> (xs : List a) -> {auto 0 _ : All (flip InBounds xs) idxs} -> List a

  Delete values from a list at specified indices. For example `deleteAt [0, 2] [5, 6, 7, 8]`
  is `[6, 8]`.
  
  @idxs The indices of the values to delete.
  @xs The list to delete values from.

Totality: total
Visibility: public export

functorIdentity : (xs : List a) -> map id xs = xs

Totality: total
Visibility: public export

data All2 : (0 _ : (a -> b -> Type)) -> List a -> List b -> Type

  A binary version of `All` from the standard library.

Totality: total
Visibility: public export
Constructors:

Nil : All2 p [] []

(::) : p x y -> All2 p xs ys -> All2 p (x :: xs) (y :: ys)

length : All2 f xs ys -> Nat

  The length of an `All2`.

Totality: total
Visibility: public export

mapProperty : (f x y -> g x y) -> All2 f xs ys -> All2 g xs ys

  Map a function over the property of an `All2`.

Totality: total
Visibility: export

forProperty : Applicative m => All2 f xs ys -> (f x y -> m (g x y)) -> m (All2 g xs ys)

  Run an effectful function over each property of an `All2`, sequencing the effects.

Totality: total
Visibility: export

data Sorted : (a -> a -> Type) -> List a -> Type

  A `Sorted f xs` proves that for all consecutive elements `x` and `y` in `xs`, `f x y` exists.
  For example, a `Sorted LT xs` proves that all `Nat`s in `xs` appear in increasing numerical
  order.

Totality: total
Visibility: public export
Constructors:

SNil : Sorted f []

  An empty list is sorted.

SOne : Sorted f [x]

  Any single element is sorted.

SCons : (y : a) -> f y x -> Sorted f (x :: xs) -> Sorted f (y :: (x :: xs))

  A list is sorted if its tail is sorted and the head is sorted w.r.t. the head of the tail.

inBoundsCons : (xs : List a) -> InBounds k xs -> InBounds k (x :: xs)

  If an index is in bounds for a list, it's also in bounds for a longer list

Totality: total
Visibility: public export