On palindromes

Défine the inductive predicate palindromic associated to lists that can be read the same way in both directions.


Look at this file .


We added to the end of this file a proof that a list is palindromic (according to the inductive definition) if and only if it is equal to its own reverse (defined by the function rev in PolyList).

This proof is quite interesting, because we needed to build some tools to achieve it :

Going home
Pierre Castéran