		Search-engine friendly clone of the ACL2 documentation.

Patbind-er

b* binder for error triples.

Usage:

(b* (((er x) (error-triple-form)))
  (result-form))

is equivalent to

(er-let* ((x (error-triple-form)))
  (result-form))

which itself is approximately equivalent to

(mv-let (erp val state)
        (error-triple-form)
   (if erp
       (mv erp val state)
     (result-form)))

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

To return a different value in case of error, the different value can be specified via :iferr:

(b* (((er x :iferr eval) (error-triple-form)))
  (result-form))

which is approximately equivalent to

(mv-let (erp val state)
        (error-triple-form)
   (if erp
       (mv erp eval state) ; note eval instead of val
     (result-form)))