		Search-engine friendly clone of the ACL2 documentation.

Error-triple

A common ACL2 programming idiom

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'' or ``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 !>

In certain settings, notably when printing evaluation results, multiple values (mv erp val state) may be considered an error triple even when val is a df rather than an ordinary object. Here is an example; see df for more about how floating-point numbers are simulated in ACL2.

ACL2 !>(mv nil (to-df 3) state)
 #d3.0
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.