		Search-engine friendly clone of the ACL2 documentation.

Char+short+int+long+llong+bool-format

Make-char+short+int+long+llong+bool-format

Basic constructor macro for char+short+int+long+llong+bool-format structures.

Syntax

(make-char+short+int+long+llong+bool-format [:uchar <uchar>] 
                                            [:schar <schar>] 
                                            [:char <char>] 
                                            [:short <short>] 
                                            [:int <int>] 
                                            [:long <long>] 
                                            [:llong <llong>] 
                                            [:bool <bool>])

This is the usual way to construct char+short+int+long+llong+bool-format structures. It simply conses together a structure with the specified fields.

This macro generates a new char+short+int+long+llong+bool-format structure from scratch. See also change-char+short+int+long+llong+bool-format, which can "change" an existing structure, instead.

Definition

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

Macro: make-char+short+int+long+llong+bool-format

(defmacro make-char+short+int+long+llong+bool-format (&rest args)
  (std::make-aggregate 'char+short+int+long+llong+bool-format
                       args
                       '((:uchar)
                         (:schar)
                         (:char)
                         (:short)
                         (:int)
                         (:long)
                         (:llong)
                         (:bool))
                       'make-char+short+int+long+llong+bool-format
                       nil))

Function: char+short+int+long+llong+bool-format

(defun char+short+int+long+llong+bool-format
       (uchar schar char short int long llong bool)
  (declare (xargs :guard (and (uchar-formatp uchar)
                              (schar-formatp schar)
                              (char-formatp char)
                              (integer-formatp short)
                              (integer-formatp int)
                              (integer-formatp long)
                              (integer-formatp llong)
                              (bool-formatp bool))))
  (declare (xargs :guard t))
  (b* ((uchar (mbe :logic (uchar-format-fix uchar)
                   :exec uchar))
       (schar (mbe :logic (schar-format-fix schar)
                   :exec schar))
       (char (mbe :logic (char-format-fix char)
                  :exec char))
       (short (mbe :logic (integer-format-fix short)
                   :exec short))
       (int (mbe :logic (integer-format-fix int)
                 :exec int))
       (long (mbe :logic (integer-format-fix long)
                  :exec long))
       (llong (mbe :logic (integer-format-fix llong)
                   :exec llong))
       (bool (mbe :logic (bool-format-fix bool)
                  :exec bool)))
    (list (cons 'uchar uchar)
          (cons 'schar schar)
          (cons 'char char)
          (cons 'short short)
          (cons 'int int)
          (cons 'long long)
          (cons 'llong llong)
          (cons 'bool bool))))