		Search-engine friendly clone of the ACL2 documentation.

Fconst-hex

Make-fconst-hex

Basic constructor macro for fconst-hex structures.

Syntax

(make-fconst-hex [:prefix <prefix>] 
                 [:core <core>] 
                 [:suffix? <suffix?>])

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

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

Definition

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

Macro: make-fconst-hex

(defmacro make-fconst-hex (&rest args)
  (std::make-aggregate 'fconst-hex
                       args '((:prefix) (:core) (:suffix?))
                       'make-fconst-hex
                       nil))

Function: fconst-hex

(defun fconst-hex (prefix core suffix?)
  (declare (xargs :guard (and (hprefixp prefix)
                              (hex-core-fconstp core)
                              (fsuffix-optionp suffix?))))
  (declare (xargs :guard t))
  (let ((__function__ 'fconst-hex))
    (declare (ignorable __function__))
    (b* ((prefix (mbe :logic (hprefix-fix prefix)
                      :exec prefix))
         (core (mbe :logic (hex-core-fconst-fix core)
                    :exec core))
         (suffix? (mbe :logic (fsuffix-option-fix suffix?)
                       :exec suffix?)))
      (cons :hex (list prefix core suffix?)))))