		Search-engine friendly clone of the ACL2 documentation.

Format-string

Make-format-string

Basic constructor macro for format-string structures.

Syntax

(make-format-string [:elements <elements>])

This is the usual way to construct format-string structures. It simply conses together a structure with the specified fields.

This macro generates a new format-string structure from scratch. See also change-format-string, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by fty::defprod.

Macro: make-format-string

(defmacro make-format-string (&rest args)
  (std::make-aggregate 'format-string
                       args '((:elements))
                       'make-format-string
                       nil))

Function: format-string

(defun format-string (elements)
 (declare (xargs :guard (char/container-listp elements)))
 (declare
  (xargs
       :guard (char/container-list-no-open/close-brace-p elements)))
 (let ((__function__ 'format-string))
  (declare (ignorable __function__))
  (b* ((elements (mbe :logic (char/container-list-fix elements)
                      :exec elements)))
   (let
    ((elements
       (mbe :logic
            (if (char/container-list-no-open/close-brace-p elements)
                elements
              nil)
            :exec elements)))
    (cons :format-string (list (cons 'elements elements)))))))