		Search-engine friendly clone of the ACL2 documentation.

Loop$-primer

Lp-section-3

Examples of FOR Loop$s

LP3: Examples of FOR Loop$s

Below is the complete log of an ACL2 session demonstrating the behavior of FOR loop$s. ACL2 also supports DO loop$s but they are not illustrated here. Note that to use loop$ one should always work in a session in which the book shown below is included. The examples below do not illustrate guards, the use of user defined functions in loop$ expressions, or proofs about loop$s.

We'll describe the syntax and semantics of loop$ in the next two sections. But we expect you can intuit the syntax and semantics of loop$ statements from these examples alone. Please try!

ACL2 !>(include-book "projects/apply/top" :dir :system)

Summary
Form:  ( INCLUDE-BOOK "projects/apply/top" ...)
Rules: NIL
Time:  1.00 seconds (prove: 0.00, print: 0.00, other: 1.00)
 "/Users/demo/books/projects/apply/top.lisp"

ACL2 !>(loop$ for x in '(a b c)
              collect (cons 'hi x))
((HI . A) (HI . B) (HI . C))

ACL2 !>(loop$ for x in '(a b c)
              when (not (eq x 'b))
              collect (cons 'hi x))
((HI . A) (HI . C))

ACL2 !>(loop$ for x in '(a b c d e f g)
              until (eq x 'd)
              collect x)
(A B C)

ACL2 !>(loop$ for x on '(a b c)
              collect x)
((A B C) (B C) (C))

ACL2 !>(loop$ for x on '(a b c)
              collect (cons (car x) (len x)))
((A . 3) (B . 2) (C . 1))

ACL2 !>(loop$ for i from 1 to 10 sum i)
55

ACL2 !>(loop$ for i from 1 to 12 by 3
              collect (* i i))
(1 16 49 100)

ACL2 !>(loop$ for x in '((a b c) (d e f) (g h i))
              collect (cons 'hi x))
((HI A B C) (HI D E F) (HI G H I))

ACL2 !>(loop$ for x in '((a b c) (d e f) (g h i))
              append (cons 'hi x))
(HI A B C HI D E F HI G H I)

ACL2 !>(loop$ for x in '(2 4 6)
              always (evenp x))
T

ACL2 !>(loop$ for x in '(2 4 5 6)
              always (evenp x))
NIL

ACL2 !>(loop$ for x in '(2 4 5 6)
              thereis (if (evenp x) nil x))
5

ACL2 !>(let ((greeting 'hi))
         (loop$ for x in '(a b c)
                collect (cons greeting x)))
((HI . A) (HI . B) (HI . C))

ACL2 !>(loop$ for x in '(a b c)
              as  y in '(65 66 67 68)
              collect (cons x y))
((A . 65) (B . 66) (C . 67))

ACL2 !>(loop$ for x in '(a b c d)
              as  y in '(65 66 67)
              collect (cons x y))
((A . 65) (B . 66) (C . 67))

ACL2 !>(loop$ for x in '((1 2 3) (4 5 6) (7 8 9))
              collect
              (loop$ for i in x collect (* i i)))
((1 4 9) (16 25 36) (49 64 81))

Now go to lp-section-4 (or return to the Table of Contents).