22 lines
480 B
Idris
22 lines
480 B
Idris
module HomeworkOne
|
|
import Data.Vect
|
|
|
|
%default total
|
|
|
|
zipW : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
|
|
zipW _ [] [] = []
|
|
zipW f (x::xs) (y::ys) = f x y :: zipWith f xs ys
|
|
|
|
lst : Vect (S n) a -> a
|
|
lst (x::[]) = x
|
|
lst (_::x::xs) = lst (x::xs)
|
|
|
|
initial : Vect (S n) a -> Vect n a
|
|
initial (x::[]) = []
|
|
initial (x1::x2::xs) = x1 :: initial (x2::xs)
|
|
|
|
palin : Eq a => Vect n a -> Bool
|
|
palin [] = True
|
|
palin [x] = True
|
|
palin (x1::l@(x2::xs)) = x1 == lst l && (palin $ initial l)
|