		Search-engine friendly clone of the ACL2 documentation.

Pinst-quote

Make-pinst-quote

Basic constructor macro for pinst-quote structures.

Syntax

(make-pinst-quote [:width <width>] 
                  [:guts <guts>])

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

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

Definition

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

Macro: make-pinst-quote

(defmacro make-pinst-quote (&rest args)
  (std::make-aggregate 'pinst-quote
                       args '((:width) (:guts))
                       'make-pinst-quote
                       nil))

Function: pinst-quote

(defun pinst-quote (width guts)
  (declare (xargs :guard (and (posp width) (pinst-p guts))))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'pinst-quote))
    (declare (ignorable acl2::__function__))
    (b* ((width (mbe :logic (acl2::pos-fix width)
                     :exec width))
         (guts (mbe :logic (pinst-fix guts)
                    :exec guts)))
      (cons :quote (std::prod-cons width guts)))))