Idris2Doc : Data.List.Elem

Data.List.Elem

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