		Search-engine friendly clone of the ACL2 documentation.

Deftrans

Deftrans-cases

Signature
(deftrans-cases) → cases
Returns: cases — Type (symbol-listp cases).

Definitions and Theorems

Function: deftrans-cases

(defun deftrans-cases nil
  (declare (xargs :guard t))
  (let ((__function__ 'deftrans-cases))
    (declare (ignorable __function__))
    '(ident ident-list const expr expr-list
            expr-option const-expr const-expr-option
            genassoc genassoc-list member-designor
            type-spec spec/qual spec/qual-list
            align-spec decl-spec decl-spec-list
            initer initer-option desiniter
            desiniter-list designor designor-list
            declor declor-option dirdeclor absdeclor
            absdeclor absdeclor-option dirabsdeclor
            dirabsdeclor-option param-declon
            param-declon-list param-declor tyname
            strunispec structdecl structdecl-list
            structdeclor structdeclor-list enumspec
            enumer enumer-list statassert initdeclor
            initdeclor-list decl decl-list
            label stmt block-item block-item-list
            fundef extdecl extdecl-list
            transunit filepath-transunit-map
            transunit-ensemble)))

Theorem: symbol-listp-of-deftrans-cases

(defthm symbol-listp-of-deftrans-cases
  (b* ((cases (deftrans-cases)))
    (symbol-listp cases))
  :rule-classes :rewrite)