Data.List

tailMismatch : Not (this = that) -> Not (There this = There that)

If the tails don't match, neither will references to them.

neitherHereNorThere : Not (x = y) -> Not (Elem x xs) -> Not (Elem x (y :: xs))

An item not in the head and not in the tail is not in the List at all

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]

hereIsNotThere : Not (Here = There later)

Here will never equal There.

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)