		Search-engine friendly clone of the ACL2 documentation.

Hex-quad

Make-hex-quad

Basic constructor macro for hex-quad structures.

Syntax

(make-hex-quad [:1st <1st>] 
               [:2nd <2nd>] 
               [:3rd <3rd>] 
               [:4th <4th>])

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

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

Definition

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

Macro: make-hex-quad

(defmacro make-hex-quad (&rest args)
  (std::make-aggregate 'hex-quad
                       args '((:1st) (:2nd) (:3rd) (:4th))
                       'make-hex-quad
                       nil))

Function: hex-quad

(defun hex-quad (1st 2nd 3rd 4th)
  (declare (xargs :guard (and (hex-digitp 1st)
                              (hex-digitp 2nd)
                              (hex-digitp 3rd)
                              (hex-digitp 4th))))
  (declare (xargs :guard t))
  (let ((__function__ 'hex-quad))
    (declare (ignorable __function__))
    (b* ((1st (mbe :logic (hex-digit-fix 1st)
                   :exec 1st))
         (2nd (mbe :logic (hex-digit-fix 2nd)
                   :exec 2nd))
         (3rd (mbe :logic (hex-digit-fix 3rd)
                   :exec 3rd))
         (4th (mbe :logic (hex-digit-fix 4th)
                   :exec 4th)))
      (cons :hex-quad (list (cons '1st 1st)
                            (cons '2nd 2nd)
                            (cons '3rd 3rd)
                            (cons '4th 4th))))))