test032.idr

module elem

import Decidable.Equality

using (xs : List a)
  data Elem  : a -> List a -> Type where
       Here  : Elem x (x :: xs)
       There : Elem x xs -> Elem x (y :: xs)

isElem : (x : Nat) -> (xs : List Nat) -> Maybe (Elem x xs)
isElem x xs = ?isElem_rhs

vadd : Num a => Vect n a -> Vect n a -> Vect n a
vadd xs ys = localZipWith (+) xs ys where
   localZipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
   localZipWith f [] [] = []
   localZipWith f (_ :: _) ys = ?localZipWith_rhs

map : (a -> b) -> Vect n a -> Vect n b
map f [] = []
map f (x :: xs) = ?maprhs

isElem2 : (x : Nat) -> (xs : List Nat) -> Maybe (Elem x xs)
isElem2 x [] = Nothing
isElem2 x (y :: ys) = ?isElem_rhs_2

isElem3 : (x : Nat) -> (xs : List Nat) -> Maybe (Elem x xs)
isElem3 x [] = Nothing
isElem3 x (y :: ys) with (decEq x y)
  isElem3 x (y :: ys) | (Yes p) = ?isElem3_rhs_1
  isElem3 x (y :: ys) | (No _) = ?isElem3_rhs_2

foo : List a -> List a
foo xs = case xs of
              xs' => ?bar