		Search-engine friendly clone of the ACL2 documentation.

Format-strings

Char-list-to-format-string

Parse the given chars into a format-string.

Signature
(char-list-to-format-string chars) → (mv erp fstring)
Arguments: chars — Guard (char-listp chars).
Returns: erp — Type (booleanp erp).; fstring — Type (format-stringp fstring).

Definitions and Theorems

Function: char-list-to-format-string

(defun char-list-to-format-string (chars)
  (declare (xargs :guard (char-listp chars)))
  (let ((__function__ 'char-list-to-format-string))
    (declare (ignorable __function__))
    (b* (((mv erp chars/containers)
          (parse-format-chars chars :base))
         ((when erp)
          (mv t *empty-format-string*)))
      (mv nil
          (make-format-string :elements chars/containers)))))

Theorem: booleanp-of-char-list-to-format-string.erp

(defthm booleanp-of-char-list-to-format-string.erp
  (b* (((mv ?erp ?fstring)
        (char-list-to-format-string chars)))
    (booleanp erp))
  :rule-classes :rewrite)

Theorem: format-stringp-of-char-list-to-format-string.fstring

(defthm format-stringp-of-char-list-to-format-string.fstring
  (b* (((mv ?erp ?fstring)
        (char-list-to-format-string chars)))
    (format-stringp fstring))
  :rule-classes :rewrite)