		Search-engine friendly clone of the ACL2 documentation.

Named-formulas

Ensure-named-formulas

Cause a soft error if the proof of any named formula fails.

Signature
(ensure-named-formulas named-formulas named-hints verbose error-erp error-val ctx state) → (mv erp val state)
Arguments: named-formulas — Named formulas to prove (an alist from names to untranslated terms).
Guard (symbol-alistp named-formulas).; named-hints — Alist from names of formulas to proof hints to prove the formulas.
Guard (symbol-truelist-alistp named-hints).; verbose — Print progress messages or not.
Guard (booleanp verbose).; error-erp — Flag to return in case of error.; error-val — Value to return in case of error.; ctx — Context for errors.
Returns: erp — error-erp or nil.; val — error-val or nil.

Use the message from the named formula proof failure as error message.

In case of error, use er-soft+ with the error flag and value passed as arguments.

Definitions and Theorems

Function: ensure-named-formulas

(defun ensure-named-formulas
       (named-formulas named-hints
                       verbose error-erp error-val ctx state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (and (symbol-alistp named-formulas)
                              (symbol-truelist-alistp named-hints)
                              (booleanp verbose))))
  (let ((__function__ 'ensure-named-formulas))
    (declare (ignorable __function__))
    (b* (((mv success msg state)
          (prove-named-formulas named-formulas
                                named-hints verbose state))
         ((unless success)
          (er-soft+ ctx error-erp error-val "~@0" msg)))
      (value nil))))