
  0 | module Data.SnocVect.Elem
  1 | 
  2 | import Data.SnocVect
  3 | import Decidable.Equality
  4 | 
  5 | %default total
  6 | 
  7 | public export
  8 | data Elem : SnocVect k a -> a -> Type where
  9 |   Here  : Elem (sx :< x) x
 10 |   There : Elem sx x -> Elem (sx :< y) x
 11 | 
 12 | export
 13 | {sx : SnocVect 0 a} -> Uninhabited (Elem sx x) where
 14 |   uninhabited Here impossible
 15 |   uninhabited (There x) impossible
 16 | 
 17 | neitherHereNorThere : DecEq a => {0 x,y : a} ->
 18 |                       Not (x = y) ->
 19 |                       Not (Elem sy x) ->
 20 |                       Not (Elem (sy :< y) x)
 21 | neitherHereNorThere _ notThere (There z) = notThere z
 22 | neitherHereNorThere notHere _ Here = notHere Refl
 23 | 
 24 | export
 25 | isElem : DecEq a => (x : a) -> (sx : SnocVect k a) -> Dec (Elem sx x)
 26 | isElem x [<] = No absurd
 27 | isElem x (sx :< y) with (decEq x y)
 28 |   isElem y (sx :< y) | (Yes Refl) = Yes Here
 29 |   isElem x (sx :< y) | (No contra) with (isElem x sx)
 30 |     isElem x (sx :< y) | (No _) | (Yes prf) = Yes (There prf)
 31 |     isElem x (sx :< y) | (No yNotX) | (No xNotInSx) =
 32 |       No (neitherHereNorThere yNotX xNotInSx)
 33 | 
 34 |