		Search-engine friendly clone of the ACL2 documentation.

Hex-pair

Make-hex-pair

Basic constructor macro for hex-pair structures.

Syntax

(make-hex-pair [:1st <1st>] 
               [:2nd <2nd>])

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

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

Definition

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

Macro: make-hex-pair

(defmacro make-hex-pair (&rest args)
  (std::make-aggregate 'hex-pair
                       args '((:1st) (:2nd))
                       'make-hex-pair
                       nil))

Function: hex-pair

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