Idris2Doc : Data.List.Elem

# 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