		Search-engine friendly clone of the ACL2 documentation.

B*-binders

Patbind-run-when

b* conditional execution operator.

Typical example: this always returns ans, but sometimes prints out warning messages:

(b* ((ans (some-computation arg1 ... argn))
     ((run-when (< ans 0))
      (cw "Warning: answer was negative?~%")
      (cw "Args were ~x0, ~x1, ..." arg1 arg2 ...)))
  ans)

Usage:

(b* (((run-when (condition-form))
      (run-form1)
      ...
      (run-formn)))
  (result-form))

is equivalent to

(prog2$ (and (condition-form)
             (progn$ (run-form1)
                     ...
                     (run-formn)))
        (result-form))