		Search-engine friendly clone of the ACL2 documentation.

Struni-spec

Make-struni-spec

Basic constructor macro for struni-spec structures.

Syntax

(make-struni-spec [:attribs <attribs>] 
                  [:name? <name?>] 
                  [:members <members>])

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

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

Definition

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

Macro: make-struni-spec

(defmacro make-struni-spec (&rest args)
  (std::make-aggregate 'struni-spec
                       args '((:attribs) (:name?) (:members))
                       'make-struni-spec
                       nil))

Function: struni-spec

(defun struni-spec (attribs name? members)
  (declare (xargs :guard (and (attrib-spec-listp attribs)
                              (ident-optionp name?)
                              (struct-declon-listp members))))
  (declare (xargs :guard t))
  (b* ((attribs (mbe :logic (attrib-spec-list-fix attribs)
                     :exec attribs))
       (name? (mbe :logic (ident-option-fix name?)
                   :exec name?))
       (members (mbe :logic (struct-declon-list-fix members)
                     :exec members)))
    (cons attribs (cons name? members))))