- data Palindrome : List a -> Type
Do geese see God?
Totality: total
Constructors:
- Empty : Palindrome []
- Single : Palindrome [_]
- Multi : Palindrome xs -> Palindrome (x :: snoc xs x)
- palindromeReverse : (xs : List a) -> Palindrome xs -> reverse xs = xs
A Palindrome reversed is itself.
Totality: total- reversePalindrome : (xs : List a) -> reverse xs = xs -> Palindrome xs
Only Palindromes are equal to their own reverse.
Totality: total