		Search-engine friendly clone of the ACL2 documentation.

B*-binders

Patbind-when

b* control flow operator.

The when binder provides a way to exit early from the sequence of computations represented by a list of b* binders.

Typical example:

(b* ((lst (some-computation arg1 arg2 ...))
     ((when (atom lst))
      ;; No entries to process, nothing to do, so just return
      ;; nil without building the expensive tbl.
      nil)
     (tbl (build-expensive-table ...)))
  (compute-expensive-result lst tbl ...))

General Form:

(b* (((when (condition-form))
      (early-form1)
      ...
      (early-formN))

     ... rest of bindings ...)
  (late-result-form))

is equivalent to

(if (condition-form)
    (progn$ (early-form1)
            ...
            (early-formN))
  (b* (... rest of bindings ...)
    (late-result-form)))

Special Case

In the special case where no early-forms are provided, the condition itself is returned. I.e.,

(b* (((when (condition-form)))
      ... rest of bindings)
  (late-result-form))

is equivalent to

(or (condition-form)
    (b* (... rest of bindings ...)
      (late-result-form)))