		Search-engine friendly clone of the ACL2 documentation.

Regaccess

Make-regaccess

Basic constructor macro for regaccess structures.

Syntax

(make-regaccess [:base <base>] 
                [:comps <comps>])

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

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

Definition

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

Macro: make-regaccess

(defmacro make-regaccess (&rest args)
  (std::make-aggregate 'regaccess
                       args '((:base) (:comps))
                       'make-regaccess
                       nil))

Function: regaccess

(defun regaccess (base comps)
  (declare (xargs :guard (and (registerp base)
                              (identifier-listp comps))))
  (declare (xargs :guard t))
  (let ((__function__ 'regaccess))
    (declare (ignorable __function__))
    (b* ((base (mbe :logic (register-fix base)
                    :exec base))
         (comps (mbe :logic (identifier-list-fix comps)
                     :exec comps)))
      (cons :regaccess (list (cons 'base base)
                             (cons 'comps comps))))))