		Search-engine friendly clone of the ACL2 documentation.

Patbind-cmp

b* binder for context-message pairs.

Usage:

(b* (((cmp x) (cmp-returning-form)))
  (result-form))

is equivalent to

(er-let*-cmp ((x (cmp-returning-form)))
  (result-form))

which itself is approximately equivalent to

(mv-let (ctx x)
        (cmp-returning-form)
   (if ctx
       (mv ctx x)
     (result-form)))

The cmp binder only makes sense as a top-level binding, but its argument may be a recursive binding.