  Iterative algorithms are traditionally expressed in ACL2 using recursion. On
the other hand, Common Lisp provides a construct, loop, which -- like most
programming languages -- provides direct support for iteration. We describe an
ACL2 analogue loop$ of loop that supports efficient ACL2 programming and
reasoning with iteration.
