- data Elem : a -> List a -> Type
A proof that some element is found in a list.
- Here : Elem x (x :: xs)
A proof that the element is at the head of the list
- There : Elem x xs -> Elem x (y :: xs)
A proof that the element is in the tail of the list
- dropElem : (xs : List a) -> Elem x xs -> List a
Remove the element at the given position.
- elemMap : (0 f : (a -> b)) -> Elem x xs -> Elem (f x) (map f xs)
Lift the membership proof to a mapped list
- elemToNat : Elem x xs -> Nat
Erase the indices, returning the numeric position of the element
- indexElem : Nat -> (xs : List a) -> Maybe (DPair a (\x => Elem x xs))
Find the element with a proof at a given position, if it is valid
- isElem : DecEq a => (x : a) -> (xs : List a) -> Dec (Elem x xs)
Check whether the given element is a member of the given list.
- neitherHereNorThere : Not (x = y) -> Not (Elem x xs) -> Not (Elem x (y :: xs))
An item not in the head and not in the tail is not in the list at all.
- thereInjective : There e1 = There e2 -> e1 = e2
- Totality: total