git.iko.soy/Idris-dev
on master help sign in
Add Data.List to base
59b9a4cEdwin Brady
libs/base/Data/List.idrnew file+28
compare with master
unifiedsplit
@@ -0,0 +1,28 @@
1+module Data.List
2+
3+%access public
4+
5+using (xs : List a)
6+ ||| A proof that some element is found in a list
7+ data Elem : a -> List a -> Type where
8+ Here : Elem x (x :: xs)
9+ There : Elem x xs -> Elem x (y :: xs)
10+
11+ instance Uninhabited (Elem {a} x []) where
12+ uninhabited Here impossible
13+ uninhabited (There p) impossible
14+
15+ private
16+ mkNo : ((x = y) -> _|_) -> (Elem x xs -> _|_) -> Elem x (y :: xs) -> _|_
17+ mkNo f g Here = f refl
18+ mkNo f g (There x) = g x
19+
20+ isElem : DecEq a => (x : a) -> (xs : List a) -> Dec (Elem x xs)
21+ isElem x [] = No absurd
22+ isElem x (y :: xs) with (decEq x y)
23+ isElem x (x :: xs) | (Yes refl) = Yes Here
24+ isElem x (y :: xs) | (No contra) with (isElem x xs)
25+ isElem x (y :: xs) | (No contra) | (Yes prf) = Yes (There prf)
26+ isElem x (y :: xs) | (No contra) | (No f) = No (mkNo contra f)
27+
28+
libs/base/base.ipkg+1
@@ -23,6 +23,7 @@ modules = System,
23 Data.Vect, Data.HVect, Data.Vect.Quantifiers,
23 Data.Vect, Data.HVect, Data.Vect.Quantifiers,
24 Data.Floats, Data.Complex, Data.Heap, Data.Fun,
24 Data.Floats, Data.Complex, Data.Heap, Data.Fun,
25 Data.Rel, Data.Buffer, Data.Erased,
25 Data.Rel, Data.Buffer, Data.Erased,
26+ Data.List,
26
27
27 Control.Isomorphism, Control.Isomorphism.Primitives,
28 Control.Isomorphism, Control.Isomorphism.Primitives,
28 Control.Monad.Identity,
29 Control.Monad.Identity,