		Search-engine friendly clone of the ACL2 documentation.

Uchar-format

Make-uchar-format

Basic constructor macro for uchar-format structures.

Syntax

(make-uchar-format [:size <size>])

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

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

Definition

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

Macro: make-uchar-format

(defmacro make-uchar-format (&rest args)
  (std::make-aggregate 'uchar-format
                       args '((:size))
                       'make-uchar-format
                       nil))

Function: uchar-format

(defun uchar-format (size)
  (declare (xargs :guard (natp size)))
  (declare (xargs :guard (>= size 8)))
  (b* ((size (mbe :logic (nfix size) :exec size)))
    (let ((size (mbe :logic (if (>= size 8) size 8)
                     :exec size)))
      (list (cons 'size size)))))