0 | module Data.List.Fresh.Elem
 1 |
 2 | import Data.List.Fresh
 3 |
 4 | %default total
 5 |
 6 | public export
 7 | data Elem : a -> FreshList a neq -> Type where
 8 |   Here  : Elem x ((x :: xs) {fresh})
 9 |   There : (pos : Elem y xs) -> Elem y ((x :: xs) {fresh})
10 |
11 | export
12 | Uninhabited (Here = There {fresh} e) where
13 |   uninhabited Refl impossible
14 |
15 | export
16 | Uninhabited (There {fresh} e = Here) where
17 |   uninhabited Refl impossible
18 |
19 | public export
20 | (.recall) : (xs : FreshList a neq) -> (pos : x `Elem` xs) -> a
21 | (x :: xs).recall Here = x
22 | (x :: xs).recall (There pos) = xs.recall pos
23 |
24 | public export
25 | recallId : (xs : FreshList a neq) -> (pos : x `Elem` xs) -> xs.recall pos = x
26 | recallId (x :: xs) Here = Refl
27 | recallId (x :: xs) (There pos) = recallId xs pos
28 |