IdrisDoc: Data.List

Data.List

isElem : DecEq a => (x : a) -> (xs : List a) -> Dec (Elem x xs)

Is the given element a member of the given list.

x

The element to be tested.

xs

The list to be checked against

intersectBy : (a -> a -> Bool) -> List a -> List a -> List a

The intersectBy function returns the intersect of two lists by user-supplied equality predicate.

intersect : Eq a => List a -> List a -> List a

Compute the intersection of two lists according to their Eq implementation.

intersect [1, 2, 3, 4] [2, 4, 6, 8]
dropElem : (xs : List a) -> (p : Elem x xs) -> List a

Remove the element at the given position.

xs

The list to be removed from

p

A proof that the element to be removed is in the list

data Elem : a -> List a -> Type

A proof that some element is found in a list.

Example: the (Elem "bar" ["foo", "bar", "baz"]) (tactics { search })

Here : Elem x (x :: xs)

A proof that the element is at the front of the list.

Example: the (Elem "a" ["a", "b"]) Here

There : (later : Elem x xs) -> Elem x (y :: xs)

A proof that the element is after the front of the list

Example: the (Elem "b" ["a", "b"]) (There Here)