data Elem : a -> SnocList a -> Type
A proof that some element is found in a list.
Here : Elem x (sx :< x)
A proof that the element is at the head of the list
There : Elem x sx -> Elem x (sx :< y)
A proof that the element is in the tail of the list
DecEq (Elem x sx)
Uninhabited (Here = There e)
Uninhabited (There e = Here)
Uninhabited (Elem x [<])
dropElem : (sx : SnocList a) -> Elem x sx -> SnocList a
Remove the element at the given position.
elemMap : (0 f : (a -> b)) -> Elem x sx -> Elem (f x) (map f sx)
Lift the membership proof to a mapped list
elemToNat : Elem x sx -> Nat
Erase the indices, returning the numeric position of the element
indexElem : Nat -> (sx : SnocList a) -> Maybe (DPair a (\x => Elem x sx))
Find the element with a proof at a given position (in reverse), if it is valid
neitherHereNorThere : Not (x = y) -> Not (Elem x sx) -> Not (Elem x (sx :< y))
An item not in the head and not in the tail is not in the list at all.