@@ -0,0 +1,31 @@
1+import System
2+import Data.List.Views
3+
4+data Palindrome : List a -> Type where
5+ PNil : Palindrome []
6+ POne : Palindrome [x]
7+ PRec : Palindrome xs -> Palindrome (x :: xs ++ [x])
8+
9+total
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
17+ Nothing => Nothing
18+ Just x => Just (PRec x)
19+ palindrome (x :: (ys ++ [y])) | (VCons z) | (No contra)
20+ = Nothing
21+
22+palinBool : DecEq a => List a -> Bool
23+palinBool xs = case palindrome xs of
24+ Nothing => False
25+ Just _ => True
26+
27+main : IO ()
28+main = do [_, num] <- getArgs
29+ let list = replicate (cast num) 'a'
30+ printLn (palinBool list)
31+