## TRACE*

trace function evaluations
Major Section: TRACE

`Trace*`

is a minor variant of `trace$`

, the ACL2 tracing utility.
See trace$ for detailed documentation.

The only difference between `trace*`

and `trace$`

is that `trace*`

provides perhaps more pleasant output, as follows. If a function is traced
without option `:entry`

or `:exit`

, then `trace*`

avoids using the name
of the so-called ``*1* function'' (also known as ``executable-counterpart
function'' or ``logic function'').

The log below illustrates the difference when using
`:set-guard-checking :none`

, which restricts execution to *1* functions.
Here we assume the following definition.

(defun fact (n)
(if (zp n)
1
(* n (fact (1- n)))))

And here is the log promised above, first showing `trace$`

and then the
(prettier output from) `trace*`

.
ACL2 >(trace$ fact)
((FACT))
ACL2 >(fact 3)
1> (ACL2_*1*_ACL2::FACT 3)
2> (ACL2_*1*_ACL2::FACT 2)
3> (ACL2_*1*_ACL2::FACT 1)
4> (ACL2_*1*_ACL2::FACT 0)
<4 (ACL2_*1*_ACL2::FACT 1)
<3 (ACL2_*1*_ACL2::FACT 1)
<2 (ACL2_*1*_ACL2::FACT 2)
<1 (ACL2_*1*_ACL2::FACT 6)
6
ACL2 >(trace* fact)
((FACT :ENTRY (CONS 'FACT ARGLIST)
:EXIT (CONS 'FACT VALUES)))
ACL2 >(fact 3)
1> (FACT 3)
2> (FACT 2)
3> (FACT 1)
4> (FACT 0)
<4 (FACT 1)
<3 (FACT 1)
<2 (FACT 2)
<1 (FACT 6)
6
ACL2 >