Commit 2020-08-13 09:22 cfcbea6e

feat(data/list/palindrome): define palindromes (#3729) This introduces an inductive type palindrome, with conversions to and from the proposition reverse l = l. Review of this PR indicates two things: (1) maybe the name is_palindrome is better, especially if we define the subtype of palindromic lists; (2) maybe defining palindrome by reverse l = l is simpler. We note these for future development.