		Search-engine friendly clone of the ACL2 documentation.

Bool-format

Make-bool-format

Basic constructor macro for bool-format structures.

Syntax

(make-bool-format [:byte-size <byte-size>] 
                  [:value-index <value-index>] 
                  [:trap <trap>])

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

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

Definition

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

Macro: make-bool-format

(defmacro make-bool-format (&rest args)
  (std::make-aggregate 'bool-format
                       args
                       '((:byte-size) (:value-index) (:trap))
                       'make-bool-format
                       nil))

Function: bool-format

(defun bool-format (byte-size value-index trap)
  (declare (xargs :guard (and (posp byte-size)
                              (natp value-index)
                              (acl2::any-p trap))))
  (declare (xargs :guard t))
  (b* ((byte-size (mbe :logic (pos-fix byte-size)
                       :exec byte-size))
       (value-index (mbe :logic (nfix value-index)
                         :exec value-index))
       (trap (mbe :logic (identity trap)
                  :exec trap)))
    (list (cons 'byte-size byte-size)
          (cons 'value-index value-index)
          (cons 'trap trap))))