git.iko.soy/Idris-dev
on fbb201c help sign in
Idris-dev/libs/base/Data/List.idr
59 lines 2.1 kB history raw
1module Data.List
3%access public
5||| A proof that some element is found in a list.
6|||
7||| Example: `the (Elem "bar" ["foo", "bar", "baz"]) (tactics { search })`
8data Elem : a -> List a -> Type where
9 ||| A proof that the element is at the front of the list.
10 |||
11 ||| Example: `the (Elem "a" ["a", "b"]) Here`
12 Here : Elem x (x :: xs)
13 ||| A proof that the element is after the front of the list
14 |||
15 ||| Example: `the (Elem "b" ["a", "b"]) (There Here)`
16 There : Elem x xs -> Elem x (y :: xs)
18instance Uninhabited (Elem {a} x []) where
19 uninhabited Here impossible
20 uninhabited (There p) impossible
22||| Is the given element a member of the given list.
23|||
24||| @x The element to be tested.
25||| @xs The list to be checked against
26isElem : DecEq a => (x : a) -> (xs : List a) -> Dec (Elem x xs)
27isElem x [] = No absurd
28isElem x (y :: xs) with (decEq x y)
29 isElem x (x :: xs) | (Yes Refl) = Yes Here
30 isElem x (y :: xs) | (No contra) with (isElem x xs)
31 isElem x (y :: xs) | (No contra) | (Yes prf) = Yes (There prf)
32 isElem x (y :: xs) | (No contra) | (No f) = No (mkNo contra f)
33 where
34 mkNo : {xs' : List a} ->
35 ((x' = y') -> Void) -> (Elem x' xs' -> Void) ->
36 Elem x' (y' :: xs') -> Void
37 mkNo f g Here = f Refl
38 mkNo f g (There x) = g x
40||| Remove the element at the given position.
41|||
42||| @xs The list to be removed from
43||| @p A proof that the element to be removed is in the list
44dropElem : (xs : List a) -> (p : Elem x xs) -> List a
45dropElem (x :: ys) Here = ys
46dropElem (x :: ys) (There p) = x :: dropElem ys p
48||| The intersectBy function returns the intersect of two lists by user-supplied equality predicate.
49intersectBy : (a -> a -> Bool) -> List a -> List a -> List a
50intersectBy eq xs ys = [x | x <- xs, any (eq x) ys]
52||| Compute the intersection of two lists according to their `Eq` instance.
53|||
54||| ```idris example
55||| intersect [1, 2, 3, 4] [2, 4, 6, 8]
56||| ```
57|||
58intersect : (Eq a) => List a -> List a -> List a
59intersect = intersectBy (==)