@@ -15,6 +15,22 @@ data Elem : a -> List a -> Type where
15 ||| Example: `the (Elem "b" ["a", "b"]) (There Here)`
15 ||| Example: `the (Elem "b" ["a", "b"]) (There Here)`
16 There : (later : Elem x xs) -> Elem x (y :: xs)
16 There : (later : Elem x xs) -> Elem x (y :: xs)
18+||| `Here` will never equal `There`.
19+hereIsNotThere : Not (Here = There _)
20+hereIsNotThere Refl impossible
22+||| If the tails don't match, neither will references to them.
23+tailMismatch : Not (this = that) -> Not (There this = There that)
24+tailMismatch f Refl = f Refl
26+implementation DecEq (Elem x xs) where
27+ decEq Here Here = Yes Refl
28+ decEq Here (There later) = No hereIsNotThere
29+ decEq (There later) Here = No (hereIsNotThere . sym)
30+ decEq (There this) (There that) with (decEq this that)
31+ decEq (There this) (There this) | Yes Refl = Yes Refl
32+ decEq (There this) (There that) | No contra = No (tailMismatch contra)
18implementation Uninhabited (Elem {a} x []) where
34implementation Uninhabited (Elem {a} x []) where
19 uninhabited Here impossible
35 uninhabited Here impossible
20 uninhabited (There p) impossible
36 uninhabited (There p) impossible