Idris2Doc : Data.List.Elem

Data.List.Elem

Elem : a -> Lista -> Type
A proof that some element is found in a list.
Totality: total
Constructors:
Here : Elemx (x::xs)
A proof that the element is at the head of the list
There : Elemxxs -> Elemx (y::xs)
A proof that the element is in the tail of the list
dropElem : (xs : Lista) -> Elemxxs -> Lista
Remove the element at the given position.
Totality: total
elemMap : (0 f : (a -> b)) -> Elemxxs -> Elem (fx) (mapfxs)
Lift the membership proof to a mapped list
Totality: total
elemToNat : Elemxxs -> Nat
Erase the indices, returning the numeric position of the element
Totality: total
indexElem : Nat -> (xs : Lista) -> Maybe (DPaira (\x => Elemxxs))
Find the element with a proof at a given position, if it is valid
Totality: total
isElem : DecEqa => (x : a) -> (xs : Lista) -> Dec (Elemxxs)
Check whether the given element is a member of the given list.
Totality: total
neitherHereNorThere : Not (x = y) -> Not (Elemxxs) -> Not (Elemx (y::xs))
An item not in the head and not in the tail is not in the list at all.
Totality: total
thereInjective : Theree1 = Theree2 -> e1 = e2
Totality: total