		Search-engine friendly clone of the ACL2 documentation.

Sdm-instruction-table-entry

Make-sdm-instruction-table-entry

Basic constructor macro for sdm-instruction-table-entry structures.

Syntax

(make-sdm-instruction-table-entry [:title <title>] 
                                  [:implemented <implemented>] 
                                  [:unimplemented <unimplemented>] 
                                  [:doc <doc>] 
                                  [:subsecs <subsecs>])

This is the usual way to construct sdm-instruction-table-entry structures. It simply conses together a structure with the specified fields.

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-sdm-instruction-table-entry

(defmacro make-sdm-instruction-table-entry (&rest args)
  (std::make-aggregate 'sdm-instruction-table-entry
                       args
                       '((:title)
                         (:implemented)
                         (:unimplemented)
                         (:doc)
                         (:subsecs))
                       'make-sdm-instruction-table-entry
                       nil))

Function: sdm-instruction-table-entry

(defun sdm-instruction-table-entry
       (title implemented unimplemented doc subsecs)
  (declare (xargs :guard (and (stringp title)
                              (inst-list-p implemented)
                              (inst-list-p unimplemented)
                              (stringp doc)
                              (sdm-instruction-table-p subsecs))))
  (declare (xargs :guard t))
  (let ((__function__ 'sdm-instruction-table-entry))
    (declare (ignorable __function__))
    (b* ((title (mbe :logic (acl2::str-fix title)
                     :exec title))
         (implemented (mbe :logic (inst-list-fix implemented)
                           :exec implemented))
         (unimplemented (mbe :logic (inst-list-fix unimplemented)
                             :exec unimplemented))
         (doc (mbe :logic (acl2::str-fix doc)
                   :exec doc))
         (subsecs (mbe :logic (sdm-instruction-table-fix subsecs)
                       :exec subsecs)))
      (list (cons 'title title)
            (cons 'implemented implemented)
            (cons 'unimplemented unimplemented)
            (cons 'doc doc)
            (cons 'subsecs subsecs)))))