list.is_palindrome

Stream: Is there code for X?

[Chris Wong]

Is there an is_palindrome : {...} -> l = reverse l somewhere in mathlib?

My use case is proving a property of Fibonacci words. Namely: every Fibonacci word is either p01 or p10 where p is a palindrome.

[Mario Carneiro]

No, but reverse l = l seems pretty clear

[Chris Wong]

That's fair. I wonder if there'd be demand for an induction principle on palindromes, as I'll probably write that at some point. Or is that too obscure?

[Kevin Buzzard]

That sounds like a funky codewars project :-)

[Kevin Buzzard]

The word palindrome doesn't seem to appear in mathlib at all.

[Scott Morrison]

Perhaps in and of itself, it's too obscure. But if you need it for something else, so one will object. We're doing maths here, the standards for "obscure" are pretty generous. :-)