		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-c-char-list

Validate a list of characters of a character constant.

Signature
(valid-c-char-list cchars prefix? ienv) → (mv erp codes)
Arguments: cchars — Guard (c-char-listp cchars).; prefix? — Guard (cprefix-optionp prefix?).; ienv — Guard (ienvp ienv).
Returns: erp — Type (maybe-msgp erp).; codes — Type (nat-listp codes).

Definitions and Theorems

Function: valid-c-char-list

(defun valid-c-char-list (cchars prefix? ienv)
  (declare (xargs :guard (and (c-char-listp cchars)
                              (cprefix-optionp prefix?)
                              (ienvp ienv))))
  (b* (((reterr) nil)
       ((when (endp cchars)) (retok nil))
       ((erp code)
        (valid-c-char (car cchars)
                      prefix? ienv))
       ((erp codes)
        (valid-c-char-list (cdr cchars)
                           prefix? ienv)))
    (retok (cons code codes))))

Theorem: maybe-msgp-of-valid-c-char-list.erp

(defthm maybe-msgp-of-valid-c-char-list.erp
  (b* (((mv acl2::?erp ?codes)
        (valid-c-char-list cchars prefix? ienv)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: nat-listp-of-valid-c-char-list.codes

(defthm nat-listp-of-valid-c-char-list.codes
  (b* (((mv acl2::?erp ?codes)
        (valid-c-char-list cchars prefix? ienv)))
    (nat-listp codes))
  :rule-classes :rewrite)

Theorem: valid-c-char-list-of-c-char-list-fix-cchars

(defthm valid-c-char-list-of-c-char-list-fix-cchars
  (equal (valid-c-char-list (c-char-list-fix cchars)
                            prefix? ienv)
         (valid-c-char-list cchars prefix? ienv)))

Theorem: valid-c-char-list-c-char-list-equiv-congruence-on-cchars

(defthm valid-c-char-list-c-char-list-equiv-congruence-on-cchars
  (implies (c-char-list-equiv cchars cchars-equiv)
           (equal (valid-c-char-list cchars prefix? ienv)
                  (valid-c-char-list cchars-equiv prefix? ienv)))
  :rule-classes :congruence)

Theorem: valid-c-char-list-of-cprefix-option-fix-prefix?

(defthm valid-c-char-list-of-cprefix-option-fix-prefix?
  (equal (valid-c-char-list cchars (cprefix-option-fix prefix?)
                            ienv)
         (valid-c-char-list cchars prefix? ienv)))

Theorem: valid-c-char-list-cprefix-option-equiv-congruence-on-prefix?

(defthm valid-c-char-list-cprefix-option-equiv-congruence-on-prefix?
  (implies (cprefix-option-equiv prefix? prefix?-equiv)
           (equal (valid-c-char-list cchars prefix? ienv)
                  (valid-c-char-list cchars prefix?-equiv ienv)))
  :rule-classes :congruence)

Theorem: valid-c-char-list-of-ienv-fix-ienv

(defthm valid-c-char-list-of-ienv-fix-ienv
  (equal (valid-c-char-list cchars prefix? (ienv-fix ienv))
         (valid-c-char-list cchars prefix? ienv)))

Theorem: valid-c-char-list-ienv-equiv-congruence-on-ienv

(defthm valid-c-char-list-ienv-equiv-congruence-on-ienv
  (implies (ienv-equiv ienv ienv-equiv)
           (equal (valid-c-char-list cchars prefix? ienv)
                  (valid-c-char-list cchars prefix? ienv-equiv)))
  :rule-classes :congruence)