		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-standardp

C-char-list-standardp

Signature
(c-char-list-standardp c-char-list) → fty::result
Arguments: c-char-list — Guard (c-char-listp c-char-list).
Returns: fty::result — Type (booleanp fty::result).

Definitions and Theorems

Function: c-char-list-standardp

(defun c-char-list-standardp (c-char-list)
  (declare (xargs :guard (c-char-listp c-char-list)))
  (let ((__function__ 'c-char-list-standardp))
    (declare (ignorable __function__))
    (cond ((endp c-char-list) t)
          (t (and (c-char-standardp (car c-char-list))
                  (c-char-list-standardp (cdr c-char-list)))))))

Theorem: booleanp-of-c-char-list-standardp

(defthm booleanp-of-c-char-list-standardp
  (b* ((fty::result (c-char-list-standardp c-char-list)))
    (booleanp fty::result))
  :rule-classes :rewrite)

Theorem: c-char-list-standardp-of-c-char-list-fix-c-char-list

(defthm c-char-list-standardp-of-c-char-list-fix-c-char-list
  (equal (c-char-list-standardp (c-char-list-fix c-char-list))
         (c-char-list-standardp c-char-list)))

Theorem: c-char-list-standardp-c-char-list-equiv-congruence-on-c-char-list

(defthm
  c-char-list-standardp-c-char-list-equiv-congruence-on-c-char-list
  (implies (c-char-list-equiv c-char-list c-char-list-equiv)
           (equal (c-char-list-standardp c-char-list)
                  (c-char-list-standardp c-char-list-equiv)))
  :rule-classes :congruence)