VALUE-TRIPLE

Major Section:  EVENTS

Examples:
(value-triple (+ 3 4))
(value-triple (cw "hi") :on-skip-proofs t)
(value-triple (@ ld-pre-eval-print))
(value-triple (@ ld-pre-eval-print) :check t)

General Form:
(value-triple form
              :on-skip-proofs sp ; optional; nil by default
              :check chk         ; optional; nil by default
              )

Value-triple provides a convenient way to evaluate a form in an event context, including progn and encapsulate and in books; see events. The form should evaluate to a single, non-stobj value.

Calls of value-triple are generally skipped when proofs are being skipped, in particular when ACL2 is performing the second pass through the events of an encapsulate form or during an include-book, or indeed any time ld-skip-proofsp is non-nil. If you want the call evaluated during those times as well, use a non-nil value for :on-skip-proofs. Note that the argument to :on-skip-proofs is not evaluated.

If you expect the form to evaluate to a non-nil value and you want an error to occur when that is not the case, you can use :check t. More generally, the argument of :check can be a form that evaluates to a single, non-stobj value. If this value is not nil, then the aforementioned test is made (that the given form is not nil). If an error occurs and the value of :check is a string or indeed any ``message'' suitable for printing by fmt when supplied as a value for tilde-directive ~@, then that string or message is printed.