Idris2Doc : Data.SnocList.Elem

Data.SnocList.Elem

Definitions

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

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

Hints:
DecEq (Elemxsx)
InjectiveThere
Uninhabited (Here=Theree)
Uninhabited (Theree=Here)
Uninhabited (Elemx [<])
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 (DPaira (\x=>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
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: export