This module defines palindromes, lists which are equal to their reverse.
The main result is the
palindrome inductive type, and its associated
principle. Also provided are conversions to and from other equivalent definitions.
palindrome, reverse, induction
palindrome l asserts that
l is a palindrome. This is defined inductively:
- The empty list is a palindrome;
- A list with one element is a palindrome;
- Adding the same element to both ends of a palindrome results in a bigger palindrome.