		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?>] 
                [:enumers <enumers>] 
                [: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?) (:enumers) (:final-comma))
                       'make-enum-spec
                       nil))

Function: enum-spec

(defun enum-spec (name? enumers final-comma)
  (declare (xargs :guard (and (ident-optionp name?)
                              (enumer-listp enumers)
                              (booleanp final-comma))))
  (declare (xargs :guard t))
  (b* ((name? (mbe :logic (ident-option-fix name?)
                   :exec name?))
       (enumers (mbe :logic (enumer-list-fix enumers)
                     :exec enumers))
       (final-comma (mbe :logic (bool-fix final-comma)
                         :exec final-comma)))
    (cons name? (cons enumers final-comma))))