		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-irrelevants

Irr-enum-spec

An irrelevant enumeration specifier.

Signature
(irr-enum-spec) → acl2::irr
Returns: acl2::irr — Type (enum-specp acl2::irr).

This can be used as a dummy value of the type.

Definitions and Theorems

Function: irr-enum-spec

(defun irr-enum-spec nil
  (declare (xargs :guard t))
  (make-enum-spec :name? nil
                  :enumers nil
                  :final-comma nil))

Theorem: enum-specp-of-irr-enum-spec

(defthm enum-specp-of-irr-enum-spec
  (b* ((acl2::irr (irr-enum-spec)))
    (enum-specp acl2::irr))
  :rule-classes :rewrite)