Power Operator for Lists

This entry defines the power operator xs ^^ n, the n-fold concatenation of xs with itself.

Much of the theory is taken from the AFP entry Combinatorics on Words Basics where the operator is called ^@. This new entry uses the standard overloaded ^^ syntax and is aimed at becoming the central theory of the power operator for lists that can be extended easily.