@@ -0,0 +1,31 @@
4+data Palindrome : List a -> Type where
7+ PRec : Palindrome xs -> Palindrome (x :: xs ++ [x])
10+palindrome : DecEq a => (xs : List a) -> Maybe (Palindrome xs)
11+palindrome xs with (vlist xs)
12+ palindrome [] | VNil = Just PNil
13+ palindrome [x] | VOne = Just POne
14+ palindrome (x :: (ys ++ [y])) | (VCons z) with (decEq x y)
15+ palindrome (y :: (ys ++ [y])) | (VCons urec) | (Yes Refl)
16+ = case palindrome ys | urec of
18+ Just x => Just (PRec x)
19+ palindrome (x :: (ys ++ [y])) | (VCons z) | (No contra)
22+palinBool : DecEq a => List a -> Bool
23+palinBool xs = case palindrome xs of
28+main = do [_, num] <- getArgs
29+ let list = replicate (cast num) 'a'
30+ printLn (palinBool list)