Data.List.Palindrome

Definitions

data Palindrome : List a -> Type

  Do geese see God?

Totality: total
Visibility: public export
Constructors:

Empty : Palindrome []

Single : Palindrome [{_:5373}]

Multi : Palindrome xs -> Palindrome (x :: snoc xs x)

palindromeReverse : (xs : List a) -> Palindrome xs -> reverse xs = xs

  A Palindrome reversed is itself.

Totality: total
Visibility: export

reversePalindrome : (xs : List a) -> reverse xs = xs -> Palindrome xs

  Only Palindromes are equal to their own reverse.

Totality: total
Visibility: export