@@ -0,0 +1,32 @@
1+module elem
2+
3+import Decidable.Equality
4+
5+using (xs : List a)
6+ data Elem : a -> List a -> Type where
7+ Here : Elem x (x :: xs)
8+ There : Elem x xs -> Elem x (y :: xs)
9+
10+isElem : (x : Nat) -> (xs : List Nat) -> Maybe (Elem x xs)
11+isElem x xs = ?isElem_rhs
12+
13+vadd : Num a => Vect n a -> Vect n a -> Vect n a
14+vadd xs ys = localZipWith (+) xs ys where
15+ localZipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
16+ localZipWith f [] [] = []
17+ localZipWith f (_ :: _) ys = ?localZipWith_rhs
18+
19+map : (a -> b) -> Vect n a -> Vect n b
20+map f [] = []
21+map f (x :: xs) = ?maprhs
22+
23+isElem2 : (x : Nat) -> (xs : List Nat) -> Maybe (Elem x xs)
24+isElem2 x [] = Nothing
25+isElem2 x (y :: ys) = ?isElem_rhs_2
26+
27+isElem3 : (x : Nat) -> (xs : List Nat) -> Maybe (Elem x xs)
28+isElem3 x [] = Nothing
29+isElem3 x (y :: ys) with (decEq x y)
30+ isElem3 x (y :: ys) | (Yes p) = ?isElem3_rhs_1
31+ isElem3 x (y :: ys) | (No _) = ?isElem3_rhs_2
32+