(deftrans-cases) → cases
Function:
(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 type-spec spec/qual spec/qual-list align-spec declspec declspec-list initer initer-option desiniter desiniter-list designor designor-list declor declor-option dirdeclor absdeclor absdeclor absdeclor-option dirabsdeclor dirabsdeclor-option paramdecl paramdecl-list paramdeclor 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:
(defthm symbol-listp-of-deftrans-cases (b* ((cases (deftrans-cases))) (symbol-listp cases)) :rule-classes :rewrite)