		Search-engine friendly clone of the ACL2 documentation.

Format-strings

Format-string-containers

Number of containers in a format string.

Signature
(format-string-containers fstring) → n
Arguments: fstring — Guard (format-stringp fstring).
Returns: n — Type (natp n).

Definitions and Theorems

Function: format-string-containers-aux

(defun format-string-containers-aux (elements)
  (declare (xargs :guard (char/container-listp elements)))
  (let ((__function__ 'format-string-containers-aux))
    (declare (ignorable __function__))
    (b* (((when (endp elements)) 0)
         (element (car elements))
         (n1 (char/container-case element
                                  :char 0
                                  :container 1))
         (n2 (format-string-containers-aux (cdr elements))))
      (+ n1 n2))))

Theorem: natp-of-format-string-containers-aux

(defthm natp-of-format-string-containers-aux
  (b* ((n (format-string-containers-aux elements)))
    (natp n))
  :rule-classes :rewrite)

Theorem: format-string-containers-aux-of-char/container-list-fix-elements

(defthm
   format-string-containers-aux-of-char/container-list-fix-elements
 (equal
   (format-string-containers-aux (char/container-list-fix elements))
   (format-string-containers-aux elements)))

Theorem: format-string-containers-aux-char/container-list-equiv-congruence-on-elements

(defthm
 format-string-containers-aux-char/container-list-equiv-congruence-on-elements
 (implies (char/container-list-equiv elements elements-equiv)
          (equal (format-string-containers-aux elements)
                 (format-string-containers-aux elements-equiv)))
 :rule-classes :congruence)

Function: format-string-containers

(defun format-string-containers (fstring)
 (declare (xargs :guard (format-stringp fstring)))
 (let ((__function__ 'format-string-containers))
  (declare (ignorable __function__))
  (format-string-containers-aux (format-string->elements fstring))))

Theorem: natp-of-format-string-containers

(defthm natp-of-format-string-containers
  (b* ((n (format-string-containers fstring)))
    (natp n))
  :rule-classes :rewrite)

Theorem: format-string-containers-of-format-string-fix-fstring

(defthm format-string-containers-of-format-string-fix-fstring
  (equal (format-string-containers (format-string-fix fstring))
         (format-string-containers fstring)))

Theorem: format-string-containers-format-string-equiv-congruence-on-fstring

(defthm
 format-string-containers-format-string-equiv-congruence-on-fstring
 (implies (format-string-equiv fstring fstring-equiv)
          (equal (format-string-containers fstring)
                 (format-string-containers fstring-equiv)))
 :rule-classes :congruence)