		Search-engine friendly clone of the ACL2 documentation.

Pinst-keypair

Make-pinst-keypair

Basic constructor macro for pinst-keypair structures.

Syntax

(make-pinst-keypair [:width <width>] 
                    [:kwd <kwd>] 
                    [:value <value>])

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

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

Definition

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

Macro: make-pinst-keypair

(defmacro make-pinst-keypair (&rest args)
  (std::make-aggregate 'pinst-keypair
                       args '((:width) (:kwd) (:value))
                       'make-pinst-keypair
                       nil))

Function: pinst-keypair

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