Idris2Doc : Data.SnocList.Elem

# Data.SnocList.Elem

## Definitions

`data Elem : a -> SnocList a -> Type`
`  A proof that some element is found in a list.`

Totality: total
Visibility: public export
Constructors:
`Here : Elem x (sx :< x)`
`  A proof that the element is at the head of the list`
`There : Elem x sx -> Elem x (sx :< y)`
`  A proof that the element is in the tail of the list`

Hints:
`DecEq (Elem x sx)`
`Injective There`
`Uninhabited (Here = There e)`
`Uninhabited (There e = Here)`
`Uninhabited (Elem x [<])`
`neitherHereNorThere : Not (x = y) -> Not (Elem x sx) -> Not (Elem x (sx :< y))`
`  An item not in the head and not in the tail is not in the list at all.`

Visibility: public export
`isElem : DecEq a => (x : a) -> (sx : SnocList a) -> Dec (Elem x sx)`
`  Check whether the given element is a member of the given list.`

Visibility: public export
`get : (sx : SnocList a) -> Elem x sx -> a`
`  Get the element at the given position.`

Visibility: public export
`lookup : (sx : SnocList a) -> Elem x sx -> Singleton x`
`  Get the element at the given position, with proof that it is the desired element.`

Visibility: public export
`dropElem : (sx : SnocList a) -> Elem x sx -> SnocList a`
`  Remove the element at the given position.`

Visibility: public export
`elemToNat : Elem x sx -> Nat`
`  Erase the indices, returning the numeric position of the element`

Visibility: public export
`indexElem : Nat -> (sx : SnocList a) -> Maybe (x : a ** Elem x sx)`
`  Find the element with a proof at a given position (in reverse), if it is valid`

Visibility: public export
`elemMap : (0 f : (a -> b)) -> Elem x sx -> Elem (f x) (map f sx)`
`  Lift the membership proof to a mapped list`

Visibility: export