		Search-engine friendly clone of the ACL2 documentation.

Format-string

Format-string->elements

Get the elements field from a format-string.

Signature
(format-string->elements x) → elements
Arguments: x — Guard (format-stringp x).
Returns: elements — Type (char/container-listp elements).

This is an ordinary field accessor created by fty::defprod.

Definitions and Theorems

Function: format-string->elements$inline

(defun format-string->elements$inline (x)
 (declare (xargs :guard (format-stringp x)))
 (declare (xargs :guard t))
 (let ((__function__ 'format-string->elements))
  (declare (ignorable __function__))
  (mbe
    :logic
    (b*
     ((x (and t x))
      (elements
           (char/container-list-fix (cdr (std::da-nth 0 (cdr x))))))
     (if (char/container-list-no-open/close-brace-p elements)
         elements
       nil))
    :exec (cdr (std::da-nth 0 (cdr x))))))

Theorem: char/container-listp-of-format-string->elements

(defthm char/container-listp-of-format-string->elements
  (b* ((elements (format-string->elements$inline x)))
    (char/container-listp elements))
  :rule-classes :rewrite)

Theorem: format-string->elements$inline-of-format-string-fix-x

(defthm format-string->elements$inline-of-format-string-fix-x
  (equal (format-string->elements$inline (format-string-fix x))
         (format-string->elements$inline x)))

Theorem: format-string->elements$inline-format-string-equiv-congruence-on-x

(defthm
 format-string->elements$inline-format-string-equiv-congruence-on-x
 (implies (format-string-equiv x x-equiv)
          (equal (format-string->elements$inline x)
                 (format-string->elements$inline x-equiv)))
 :rule-classes :congruence)