git.iko.soy/Idris-dev
on bf4e535 help sign in
Idris-dev/test/interactive001/test032.idr
36 lines 1.0 kB history raw
1module elem
3import Decidable.Equality
4import Data.Vect
6using (xs : List a)
7 data Elem : a -> List a -> Type where
8 Here : Elem x (x :: xs)
9 There : Elem x xs -> Elem x (y :: xs)
11isElem : (x : Nat) -> (xs : List Nat) -> Maybe (Elem x xs)
12isElem x xs = ?isElem_rhs
14vadd : Num a => Vect n a -> Vect n a -> Vect n a
15vadd xs ys = localZipWith (+) xs ys where
16 localZipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
17 localZipWith f [] [] = []
18 localZipWith f (_ :: _) ys = ?localZipWith_rhs
20map : (a -> b) -> Vect n a -> Vect n b
21map f [] = []
22map f (x :: xs) = ?maprhs
24isElem2 : (x : Nat) -> (xs : List Nat) -> Maybe (Elem x xs)
25isElem2 x [] = Nothing
26isElem2 x (y :: ys) = ?isElem_rhs_2
28isElem3 : (x : Nat) -> (xs : List Nat) -> Maybe (Elem x xs)
29isElem3 x [] = Nothing
30isElem3 x (y :: ys) with (decEq x y)
31 isElem3 x (y :: ys) | (Yes p) = ?isElem3_rhs_1
32 isElem3 x (y :: ys) | (No _) = ?isElem3_rhs_2
34foo : List a -> List a
35foo xs = case xs of
36 xs' => ?bar