Zulip Chat Archive

Stream: Is there code for X?

Topic: list.is_palindrome


view this post on Zulip Chris Wong (Apr 19 2020 at 00:00):

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.

view this post on Zulip Mario Carneiro (Apr 19 2020 at 00:02):

No, but reverse l = l seems pretty clear

view this post on Zulip Chris Wong (Apr 19 2020 at 00:09):

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?

view this post on Zulip Kevin Buzzard (Apr 19 2020 at 00:11):

That sounds like a funky codewars project :-)

view this post on Zulip Kevin Buzzard (Apr 19 2020 at 00:11):

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

view this post on Zulip Scott Morrison (Apr 19 2020 at 00:11):

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. :-)


Last updated: May 07 2021 at 22:14 UTC