Idris2Doc : Data.SnocList.Elem



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

Totality: total
Visibility: public export
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

DecEq (Elemxsx)
Uninhabited (Here=Theree)
Uninhabited (Theree=Here)
Uninhabited (Elemx [<])
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.

Visibility: public export
isElem : DecEqa=> (x : a) -> (sx : SnocLista) ->Dec (Elemxsx)
  Check whether the given element is a member of the given list.

Visibility: public export
get : (sx : SnocLista) ->Elemxsx->a
  Get the element at the given position.

Visibility: public export
lookup : (sx : SnocLista) ->Elemxsx->Singletonx
  Get the element at the given position, with proof that it is the desired element.

Visibility: public export
dropElem : (sx : SnocLista) ->Elemxsx->SnocLista
  Remove the element at the given position.

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

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

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

Visibility: export