Idris2Doc : Data.List1.Elem

# Data.List1.Elem

## Definitions

`data Elem : a -> List1 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 (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 : List1 a) -> Dec (Elem x xs)`
`  Check whether the given element is a member of the given list.`

Totality: total
Visibility: public export
`dropElem : (xs : List1 a) -> Elem x xs -> List a`
`  Remove the element at the given position. Forgets that the list is  non-empty, since there is no guarantee that it will remain non-empty after  the removal.`

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 : List1 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