Palindromes
This module defines palindromes, lists which are equal to their reverse.
The main result is the palindrome inductive type, and its associated palindrome.rec_on induction
principle. Also provided are conversions to and from other equivalent definitions.
References
Tags
palindrome, reverse, induction
- nil : ∀ {α : Type u_1}, palindrome list.nil
- singleton : ∀ {α : Type u_1} (x : α), palindrome [x]
- cons_concat : ∀ {α : Type u_1} (x : α) {l : list α}, palindrome l → palindrome (x :: (l ++ [x]))
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.
@[instance]