		Search-engine friendly clone of the ACL2 documentation.

Error-checking

Ensure-string-or-nil

Cause an error if a value is not a string or nil.

Signature
(ensure-string-or-nil x description error-erp error-val ctx state) → (mv erp val state)
Arguments: x — Value to check.; 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-string-or-nil

(defun ensure-string-or-nil
       (x description
          error-erp error-val ctx state)
       (declare (xargs :stobjs (state)))
       (declare (xargs :guard (msgp description)))
       (b* (((unless (maybe-stringp x))
             (er-soft+ ctx error-erp
                       error-val "~@0 must be a string or NIL."
                       description)))
           (value nil)))

Theorem: return-type-of-ensure-string-or-nil.erp

(defthm return-type-of-ensure-string-or-nil.erp
        (b* (((mv ?erp ?val ?state)
              (ensure-string-or-nil x description
                                    error-erp error-val ctx state)))
            (implies erp (equal erp error-erp)))
        :rule-classes :rewrite)

Theorem: return-type-of-ensure-string-or-nil.val

(defthm return-type-of-ensure-string-or-nil.val
        (b* (((mv ?erp ?val ?state)
              (ensure-string-or-nil x 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-string-or-nil$: Calls ensure-string-or-nil with ctx and state as the last two arguments.