		Search-engine friendly clone of the ACL2 documentation.

Hints-specifier

Canonicalize-hints-specifier

Turn a hints specifier into an equivalent canonical one.

Signature
(canonicalize-hints-specifier x legal-kwds) → cx
Returns: cx — Type (canonical-hints-specifier-p cx legal-kwds), given the guard.

If the hints specifier is already canonical, it is left unchanged. Otherwise, the abbreviation is “expanded”.

Definitions and Theorems

Function: canonicalize-hints-specifier

(defun canonicalize-hints-specifier (x legal-kwds)
  (declare (xargs :guard (and (keyword-listp legal-kwds)
                              (no-duplicatesp-eq legal-kwds)
                              (hints-specifier-p x legal-kwds))))
  (let ((__function__ 'canonicalize-hints-specifier))
    (declare (ignorable __function__))
    (cond ((canonical-hints-specifier-p x legal-kwds)
           x)
          (t (acl2::make-keyword-value-list-from-keys-and-value
                  legal-kwds x)))))

Theorem: return-type-of-canonicalize-hints-specifier

(defthm return-type-of-canonicalize-hints-specifier
 (implies
  (and
     (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)
     (hints-specifier-p x legal-kwds))
  (b* ((cx (canonicalize-hints-specifier x legal-kwds)))
    (canonical-hints-specifier-p cx legal-kwds)))
 :rule-classes :rewrite)