Util

Miscellaneous library utilities.

Reexports

Definitions

dflip : {0 c : a -> b -> Type} -> ((x : a) -> (y : b) -> c x y) -> (y : b) -> (x : a) -> c x y

  A dependent variant of `flip` where the return type can depend on the input values. `dflip`
  flips the order of arguments for a function, such that `dflip f x y` is the same as `f y x`.

Totality: total
Visibility: public export

0 Neq : Nat -> Nat -> Type

  A `Neq x y` proves `x` is not equal to `y`.

Totality: total
Visibility: public export

range : (n : Nat) -> Vect n Nat

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

Totality: total
Visibility: export

enumerate : Vect n a -> Vect n (Nat, a)

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

Totality: total
Visibility: export

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

map : ((x : a) -> b) -> (xs : List a) -> {auto 0 _ : All p xs} -> List b

  Map a constrained function over a list given a list of constraints.

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

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)

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

(>$<) : (env' -> env) -> ReaderT env m a -> ReaderT env' m a

  Apply a function to the environment of a reader.

Totality: total
Visibility: export
Fixity Declaration: infixl operator, level 4