		Search-engine friendly clone of the ACL2 documentation.

Enumspec

Make-enumspec

Basic constructor macro for enumspec structures.

Syntax

(make-enumspec [:name <name>] 
               [:list <list>] 
               [:final-comma <final-comma>])

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

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

Definition

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

Macro: make-enumspec

(defmacro make-enumspec (&rest args)
  (std::make-aggregate 'enumspec
                       args '((:name) (:list) (:final-comma))
                       'make-enumspec
                       nil))

Function: enumspec

(defun enumspec (name list final-comma)
  (declare (xargs :guard (and (ident-optionp name)
                              (enumer-listp list)
                              (booleanp final-comma))))
  (declare (xargs :guard t))
  (let ((__function__ 'enumspec))
    (declare (ignorable __function__))
    (b* ((name (mbe :logic (ident-option-fix name)
                    :exec name))
         (list (mbe :logic (enumer-list-fix list)
                    :exec list))
         (final-comma (mbe :logic (bool-fix final-comma)
                           :exec final-comma)))
      (list (cons 'name name)
            (cons 'list list)
            (cons 'final-comma final-comma)))))