Data.Linear.List

Reexports

Definitions

filter1 : (a -> F1 s Bool) -> List a -> F1 s (List a)

  Filters a list using a predicate based on mutable
  linear state.

Totality: total
Visibility: export

find1 : (a -> F1 s Bool) -> List a -> F1 s (Maybe a)

  Returns the first value in a list, for which the given
  linear predicate returns `True`.

Totality: total
Visibility: export

any1 : (a -> F1 s Bool) -> List a -> F1 s Bool

  Returns `True` if the given list holds at least one value,
  for which the given linear predicate returns `True`
  
  Trivially, this returns `False` for the empty list.

Totality: total
Visibility: export

all1 : (a -> F1 s Bool) -> List a -> F1 s Bool

  Returns `True` if the given list holds only values,
  for which the given linear predicate returns `True`
  
  Trivially, this returns `True` for the empty list.

Totality: total
Visibility: export

span1 : (a -> F1 s Bool) -> List a -> F1 s (List a, List a)

  Returns the longest (possibly empty) prefix of the given list
  for which the given predicate returns `True`.
  
  The second value of the pair returns the remainder of
  the list.

Totality: total
Visibility: export

break1 : (a -> F1 s Bool) -> List a -> F1 s (List a, List a)

  Like `span1` but returns the longest prefix, for which the
  predicate does *not* hold.

Totality: total
Visibility: export

partition1 : (a -> F1 s Bool) -> List a -> F1 s (List a, List a)

  Partitions the values in a list according to the given
  linear predicate.
  
  Returns a pair of lists, the first of which holds the values
  for which the predicate returned `False`. All other values
  are returned in the second list.

Totality: total
Visibility: export

mapMaybe1 : (a -> F1 s (Maybe b)) -> List a -> F1 s (List b)

  Using a `Maybe` function to map and filter a list in one go.

Totality: total
Visibility: export

replicate1 : Nat -> F1 s a -> F1 s (List a)

  Fills a list with values from a stateful linear computation.

Totality: total
Visibility: export