Data.SnocVect.Elem

Definitions

data Elem : SnocVect k a -> a -> Type

Totality: total
Visibility: public export
Constructors:

Here : Elem (sx :< x) x

There : Elem sx x -> Elem (sx :< y) x

Hint: 

Uninhabited (Elem sx x)

isElem : DecEq a => (x : a) -> (sx : SnocVect k a) -> Dec (Elem sx x)

Totality: total
Visibility: export