		Search-engine friendly clone of the ACL2 documentation.

Trace$

Trace*

Trace* is a beginner-friendly variant of trace$, the ACL2 tracing utility.

See trace$ for more documentation and advanced functionality.

Trace* should be used with :set-guard-checking :none and should not be used to trace built-in functions.

The log below illustrates the differences between trace* and trace$:

ACL2 p>
(defun app (x y)
  (if (endp x)
    y
    (cons (car x) (app (cdr x) y))))
...
 APP
ACL2 p>(trace$ app)
 ((APP))
ACL2 p>(app (list 1 2) (list 3))
1> (ACL2_*1*_ACL2::APP (1 2) (3))
  2> (ACL2_*1*_ACL2::APP (2) (3))
    3> (ACL2_*1*_ACL2::APP NIL (3))
    <3 (ACL2_*1*_ACL2::APP (3))
  <2 (ACL2_*1*_ACL2::APP (2 3))
<1 (ACL2_*1*_ACL2::APP (1 2 3))
(1 2 3)
ACL2 p>(trace* app)
 (APP)
ACL2 p>(app (list 1 2) (list 3))
1> (APP (LIST 1 2) (LIST 3))
  2> (APP (LIST 2) (LIST 3))
    3> (APP NIL (LIST 3))
    <3 (APP NIL (LIST 3))
     = (LIST 3)
  <2 (APP (LIST 2) (LIST 3))
   = (LIST 2 3)
<1 (APP (LIST 1 2) (LIST 3))
 = (LIST 1 2 3)
(1 2 3)
ACL2 p>