		Search-engine friendly clone of the ACL2 documentation.

Error-checking

Ensure-symbol-different

Cause an error if a symbol is the same as another symbol.

Signature
(ensure-symbol-different symb symb1 description1 description error-erp error-val ctx state) → (mv erp val state)
Arguments: symb — Symbol to check.
Guard (symbolp symb).; symb1 — Symbol that symb must be different from.
Guard (symbolp symb1).; description1 — Description of symb1, for the error message.
Guard (msgp description1).; 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-symbol-different

(defun ensure-symbol-different (symb symb1 description1 description
                                     error-erp error-val ctx state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (and (symbolp symb)
                              (symbolp symb1)
                              (msgp description1)
                              (msgp description))))
  (b* (((when (eq symb symb1))
        (er-soft+ ctx error-erp error-val
                  "~@0 must be different from ~@1."
                  description description1)))
    (value nil)))

Theorem: return-type-of-ensure-symbol-different.erp

(defthm return-type-of-ensure-symbol-different.erp
  (b* (((mv ?erp ?val ?state)
        (ensure-symbol-different symb symb1 description1 description
                                 error-erp error-val ctx state)))
    (implies erp (equal erp error-erp)))
  :rule-classes :rewrite)

Theorem: return-type-of-ensure-symbol-different.val

(defthm return-type-of-ensure-symbol-different.val
  (b* (((mv ?erp ?val ?state)
        (ensure-symbol-different symb symb1 description1 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-symbol-different$: Calls ensure-symbol-different with ctx and state as the last two arguments.