		Search-engine friendly clone of the ACL2 documentation.

Proof-builder-commands

ACL2-pc::print

(macro) print the result of evaluating the given form

Example:
(print (append '(a b) '(c d)))
Print the list (a b c d) to the terminal

General Forms:
(print form)
(print form t)

Prettyprints the result of evaluating form. The evaluation of form should return a single value that is not state or a single-threaded object (see stobj). The optional second argument causes printing to be done without elision (so-called ``evisceration''; see evisc-tuple).

If the form you want to evaluate does not satisfy the criterion above, you should create an appropriate call of the lisp command instead. Notice that this command always returns (mv nil nil state) where the second result will always be REPLACED-STATE.