Data.List.Elem

Definitions

data Elem : a -> List a -> Type

  A proof that some element is found in a list.

Totality: total
Visibility: public export
Constructors:

Here : Elem x (x :: xs)

  A proof that the element is at the head of the list

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

  A proof that the element is in the tail of the list

Hints:

DecEq (Elem x xs)

Injective There

Uninhabited (Here = There e)

Uninhabited (There e = Here)

Uninhabited (Elem x [])

Uninhabited (x = z) => Uninhabited (Elem z xs) => Uninhabited (Elem z (x :: xs))

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.

Totality: total
Visibility: export

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

  Check whether the given element is a member of the given list.

Totality: total
Visibility: public export

get : (xs : List a) -> Elem x xs -> a

  Get the element at the given position.

Totality: total
Visibility: public export

lookup : (xs : List a) -> Elem x xs -> Singleton x

  Get the element at the given position, with proof that it is the desired element.

Totality: total
Visibility: public export

dropElem : (xs : List a) -> Elem x xs -> List a

  Remove the element at the given position.

Totality: total
Visibility: public export

elemToNat : Elem x xs -> Nat

  Erase the indices, returning the numeric position of the element

Totality: total
Visibility: public export

indexElem : Nat -> (xs : List a) -> Maybe (x : a ** Elem x xs)

  Find the element with a proof at a given position, if it is valid

Totality: total
Visibility: public export

elemMap : (0 f : (a -> b)) -> Elem x xs -> Elem (f x) (map f xs)

  Lift the membership proof to a mapped list

Totality: total
Visibility: export