test032.idr

module elem

import Decidable.Equality
import Data.Vect

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

elemVoid1 : elem.Elem x [] -> Void
elemVoid1 x = ?elemVoid1_rhs

elemVoid2 : elem.Elem x [] -> Void
elemVoid2 x = case x of
                   case_val => ?elemVoid2_rhs