		Search-engine friendly clone of the ACL2 documentation.

Enum-spec

Make-enum-spec

Basic constructor macro for enum-spec structures.

Syntax

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

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

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

Definition

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

Macro: make-enum-spec

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

Function: enum-spec

(defun enum-spec (name list final-comma)
  (declare (xargs :guard (and (ident-optionp name)
                              (enumer-listp list)
                              (booleanp final-comma))))
  (declare (xargs :guard t))
  (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)))
    (cons name (cons list final-comma))))