nil
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.
