Idris2Doc : Data.SnocList.Elem

Data.SnocList.Elem

dataElem : a -> SnocLista -> Type
  A proof that some element is found in a list.

Totality: total
Constructors:
Here : Elemx (sx:<x)
  A proof that the element is at the head of the list
There : Elemxsx -> Elemx (sx:<y)
  A proof that the element is in the tail of the list
dropElem : (sx : SnocLista) -> Elemxsx -> SnocLista
  Remove the element at the given position.

elemMap : (0 f : (a -> b)) -> Elemxsx -> Elem (fx) (mapfsx)
  Lift the membership proof to a mapped list

elemToNat : Elemxsx -> Nat
  Erase the indices, returning the numeric position of the element

indexElem : Nat -> (sx : SnocLista) -> Maybe (DPaira (\x => Elemxsx))
  Find the element with a proof at a given position (in reverse), if it is valid

neitherHereNorThere : Not (x = y) -> Not (Elemxsx) -> Not (Elemx (sx:<y))
  An item not in the head and not in the tail is not in the list at all.

thereInjective : Theree1 = Theree2 -> e1 = e2