lisp command
instead. Notice that this command always returns
(mv nil nil state) where the second result will always be
REPLACED-STATE.
print the result of evaluating the given form
Major Section: PROOF-CHECKER-COMMANDS
Example: (print (append '(a b) '(c d))) Print the list (a b c d) to the terminalPrettyprints the result of evaluating form. The evaluation ofGeneral Form: (print form)
form
should return a single value that is not state or a single-threaded
object (see stobj).
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.