Email Gateway (Feb 23 2025 at 00:55): Email Gateway (Feb 23 2025 at 00:55):From: Gerwin Klein <cl-isabelle-users@lists.cam.ac.uk>
Power Operator for Lists
by Štěpán Holub, Martin Raška, Štěpán Starosta and Tobias Nipkow
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.
https://www.isa-afp.org/entries/List_Power.html
Enjoy!
Gerwin
Last updated: Mar 09 2025 at 12:28 UTC