		Search-engine friendly clone of the ACL2 documentation.

Ensure-is-hints-specifier

Cause an error if a value is not a hints specifier.

Signature
(ensure-is-hints-specifier x legal-kwds description error-erp error-val ctx state) → (mv erp val state)
Arguments: x — Value to check.; legal-kwds — Guard (and (keyword-listp legal-kwds) (no-duplicatesp-eq legal-kwds)).; description — Guard (msgp description).; error-erp — Flag to return in case of error.; error-val — Value to return in case of error.; ctx — Context for errors.
Returns: erp — Type (implies erp (equal erp error-erp)).; val — Type (and (implies erp (equal val error-val)) (implies (and (not erp) error-erp) (canonical-hints-specifier-p val legal-kwds))) , given the guard.

Definitions and Theorems

Function: ensure-is-hints-specifier

(defun ensure-is-hints-specifier (x legal-kwds description
                                    error-erp error-val ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (and (keyword-listp legal-kwds)
                                  (no-duplicatesp-eq legal-kwds))
                             (msgp description))))
 (b*
  (((unless (hints-specifier-p x legal-kwds))
    (er-soft+
     ctx error-erp error-val
     "~@0 must be an APT hints specifier.  See :DOC APT::HINTS-SPECIFIER."
     description)))
  (value (canonicalize-hints-specifier x legal-kwds))))

Theorem: return-type-of-ensure-is-hints-specifier.erp

(defthm return-type-of-ensure-is-hints-specifier.erp
  (b* (((mv ?erp ?val acl2::?state)
        (ensure-is-hints-specifier x legal-kwds description
                                   error-erp error-val ctx state)))
    (implies erp (equal erp error-erp)))
  :rule-classes :rewrite)

Theorem: return-type-of-ensure-is-hints-specifier.val

(defthm return-type-of-ensure-is-hints-specifier.val
 (implies
  (and
    (state-p state)
    (if
     (keyword-listp legal-kwds)
     ((lambda (acl2::x)
        (return-last
             'acl2::mbe1-raw
             (acl2::no-duplicatesp-eq-exec acl2::x)
             (return-last
                  'progn
                  (acl2::no-duplicatesp-eq-exec$guard-check acl2::x)
                  (no-duplicatesp-equal acl2::x))))
      legal-kwds)
     'nil)
    (msgp description))
  (b* (((mv ?erp ?val acl2::?state)
        (ensure-is-hints-specifier x legal-kwds description
                                   error-erp error-val ctx state)))
    (and (implies erp (equal val error-val))
         (implies (and (not erp) error-erp)
                  (canonical-hints-specifier-p val legal-kwds)))))
 :rule-classes :rewrite)

Subtopics

Ensure-is-hints-specifier$: Calls ensure-is-hints-specifier with ctx and state as the last two arguments.