a common ACL2 programming idiom
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
ACL2 !>(mv nil (+ 3 4) state) ; error triple, error component of nil
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.