Add Elem get and lookup functions

libs/base/Data/List/Elem.idr

@@ -1,5 +1,6 @@
 module Data.List.Elem
 
+import Data.Singleton
 import Decidable.Equality
 import Control.Function
 
@@ -62,6 +63,18 @@ isElem x (y :: xs) with (decEq x y)
     isElem x (y :: xs) | No xny | Yes xxs = Yes (There xxs)
     isElem x (y :: xs) | No xny | No xnxs = No (neitherHereNorThere xny xnxs)
 
+||| Get the element at the given position.
+public export
+get : (xs : List a) -> (p : Elem x xs) -> a
+get (x :: _) Here = x
+get (_ :: xs) (There p) = get xs p
+
+||| Get the element at the given position, with proof that it is the desired element.
+public export
+lookup : (xs : List a) -> (p : Elem x xs) -> Singleton x
+lookup (x :: _) Here = Val x
+lookup (_ :: xs) (There p) = lookup xs p
+
 ||| Remove the element at the given position.
 public export
 dropElem : (xs : List a) -> (p : Elem x xs) -> List a

libs/base/Data/SnocList/Elem.idr

@@ -1,5 +1,6 @@
 module Data.SnocList.Elem
 
+import Data.Singleton
 import Data.SnocList
 import Decidable.Equality
 import Control.Function
@@ -20,21 +21,49 @@ export
 Uninhabited (There e = Here) where
   uninhabited Refl impossible
 
-export
-Uninhabited (Elem {a} x [<]) where
-  uninhabited Here impossible
-  uninhabited (There p) impossible
-
 export
 Injective (There {x} {y} {sx}) where
   injective Refl = Refl
 
 export
-DecEq (x `Elem` sx) where
+DecEq (Elem x sx) where
   decEq Here Here = Yes Refl
-  decEq (There y) (There z) = decEqCong $ decEq y z
-  decEq Here (There _) = No absurd
-  decEq (There _) Here = No absurd
+  decEq (There this) (There that) = decEqCong $ decEq this that
+  decEq Here (There later) = No absurd
+  decEq (There later) Here = No absurd
+
+public export
+Uninhabited (Elem {a} x [<]) where
+  uninhabited Here impossible
+  uninhabited (There p) impossible
+
+||| An item not in the head and not in the tail is not in the list at all.
+public export
+neitherHereNorThere : Not (x = y) -> Not (Elem x sx) -> Not (Elem x (sx :< y))
+neitherHereNorThere xny _ Here = xny Refl
+neitherHereNorThere _ xnxs (There xxs) = xnxs xxs
+
+||| Check whether the given element is a member of the given list.
+public export
+isElem : DecEq a => (x : a) -> (sx : SnocList a) -> Dec (Elem x sx)
+isElem x [<] = No absurd
+isElem x (sx :< y) with (decEq x y)
+  isElem x (sx :< x) | Yes Refl = Yes Here
+  isElem x (sx :< y) | No xny with (isElem x sx)
+    isElem x (sx :< y) | No xny | Yes xsx = Yes (There xsx)
+    isElem x (sx :< y) | No xny | No xnsx = No (neitherHereNorThere xny xnsx)
+
+||| Get the element at the given position.
+public export
+get : (sx : SnocList a) -> (p : Elem x sx) -> a
+get (_ :< x) Here = x
+get (sx :< _) (There p) = get sx p
+
+||| Get the element at the given position, with proof that it is the desired element.
+public export
+lookup : (sx : SnocList a) -> (p : Elem x sx) -> Singleton x
+lookup (_ :< x) Here = Val x
+lookup (sx :< _) (There p) = lookup sx p
 
 ||| Remove the element at the given position.
 public export
@@ -60,9 +89,3 @@ export
 elemMap : (0 f : a -> b) -> Elem x sx -> Elem (f x) (map f sx)
 elemMap f Here = Here
 elemMap f (There el) = There $ elemMap f el
-
-||| An item not in the head and not in the tail is not in the list at all.
-export
-neitherHereNorThere : Not (x = y) -> Not (Elem x sx) -> Not (Elem x (sx :< y))
-neitherHereNorThere xny _ Here = xny Refl
-neitherHereNorThere _ xnxs (There xxs) = xnxs xxs

libs/base/Data/Vect/Elem.idr

@@ -1,5 +1,6 @@
 module Data.Vect.Elem
 
+import Data.Singleton
 import Data.Vect
 import Decidable.Equality
 
@@ -23,6 +24,17 @@ export
 Uninhabited (There e = Here) where
   uninhabited Refl impossible
 
+export
+Injective (There {x} {y} {xs}) where
+  injective Refl = Refl
+
+export
+DecEq (Elem x xs) where
+  decEq Here Here = Yes Refl
+  decEq (There this) (There that) = decEqCong $ decEq this that
+  decEq Here (There later) = No absurd
+  decEq (There later) Here = No absurd
+
 export
 Uninhabited (Elem x []) where
   uninhabited Here impossible
@@ -48,6 +60,18 @@ isElem x (y::xs) with (decEq x y)
     isElem x (y::xs) | (No xneqy) | (Yes xinxs) = Yes (There xinxs)
     isElem x (y::xs) | (No xneqy) | (No xninxs) = No (neitherHereNorThere xneqy xninxs)
 
+||| Get the element at the given position.
+public export
+get : (xs : Vect n a) -> (p : Elem x xs) -> a
+get (x :: _) Here = x
+get (_ :: xs) (There p) = get xs p
+
+||| Get the element at the given position, with proof that it is the desired element.
+public export
+lookup : (xs : Vect n a) -> (p : Elem x xs) -> Singleton x
+lookup (x :: _) Here = Val x
+lookup (_ :: xs) (There p) = lookup xs p
+
 public export
 replaceElem : (xs : Vect k t) -> Elem x xs -> (y : t) -> (ys : Vect k t ** Elem y ys)
 replaceElem (x::xs) Here y = (y :: xs ** Here)