Major Section: STATE
When evaluation returns three values, where the first two are ordinary
(non-stobj) objects and the third is the ACL2 state, the result may
be called an ``error triple''. If an error triple is (mv erp val state),
we think of erp as an error flag and val as the returned value.
By default, if the result of evaluating a top-level form is an error triple
(mv erp val state), then that result is not printed if erp is
non-nil or if val is the keyword :INVISIBLE, and otherwise
val is printed with a preceding space. For example:
ACL2 !>(+ 3 4) ; ordinary value 7 ACL2 !>(mv nil (+ 3 4) state) ; error triple, error component of nil 7 ACL2 !>(mv t (+ 3 4) state) ; error triple, non-nil error component ACL2 !>(mv nil :invisible state) ; special case for :INVISIBLE ACL2 !>
See programming-with-state for a discussion of error triples and how to
program with them. Also see ld-error-triples and see ld for a discussion
of the value :COMMAND-CONVENTIONS for keyword
:LD-POST-EVAL-PRINT.
