		Search-engine friendly clone of the ACL2 documentation.

Error-checking

Ensure-list-has-no-duplicates

Cause an error if a list has duplicates.

Signature
(ensure-list-has-no-duplicates list description error-erp error-val ctx state) → (mv erp val state)
Arguments: list — List to check.
Guard (true-listp list).; 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) (not val))) .

Definitions and Theorems

Function: ensure-list-has-no-duplicates

(defun ensure-list-has-no-duplicates
       (list description
             error-erp error-val ctx state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (and (true-listp list)
                              (msgp description))))
  (b* (((unless (no-duplicatesp-equal list))
        (er-soft+ ctx error-erp
                  error-val "~@0 must have no duplicates."
                  description)))
    (value nil)))

Theorem: return-type-of-ensure-list-has-no-duplicates.erp

(defthm return-type-of-ensure-list-has-no-duplicates.erp
  (b*
   (((mv ?erp ?val ?state)
     (ensure-list-has-no-duplicates list description
                                    error-erp error-val ctx state)))
   (implies erp (equal erp error-erp)))
  :rule-classes :rewrite)

Theorem: return-type-of-ensure-list-has-no-duplicates.val

(defthm return-type-of-ensure-list-has-no-duplicates.val
  (b*
   (((mv ?erp ?val ?state)
     (ensure-list-has-no-duplicates list description
                                    error-erp error-val ctx state)))
   (and (implies erp (equal val error-val))
        (implies (and (not erp) error-erp)
                 (not val))))
  :rule-classes :rewrite)

Subtopics

Ensure-list-has-no-duplicates$: Calls ensure-list-has-no-duplicates with ctx and state as the last two arguments.