		Search-engine friendly clone of the ACL2 documentation.

Defmake-self-event-generation

Defmake-self-gen-sum-cases

Generate the code for the cases of a sum type.

Signature
(defmake-self-gen-sum-cases type prods member-names fty-table make-self-table) → keyword+term-list
Arguments: type — Guard (symbolp type).; prods — Guard (flexprod-listp prods).; member-names — Guard (symbol-listp member-names).; fty-table — Guard (alistp fty-table).; make-self-table — Guard (alistp make-self-table).
Returns: keyword+term-list — Type (true-listp keyword+term-list).

Definitions and Theorems

Function: defmake-self-gen-sum-cases

(defun defmake-self-gen-sum-cases
       (type prods
             member-names fty-table make-self-table)
 (declare (xargs :guard (and (symbolp type)
                             (flexprod-listp prods)
                             (symbol-listp member-names)
                             (alistp fty-table)
                             (alistp make-self-table))))
 (let ((__function__ 'defmake-self-gen-sum-cases))
  (declare (ignorable __function__))
  (b* (((when (endp prods)) nil)
       (prod (car prods))
       (kind (flexprod->kind prod))
       ((unless (keywordp kind))
        (raise "Internal error: kind ~x0 is not a keyword."
               kind)))
   (list* kind
          (defmake-self-gen-sum-case
               type prod
               member-names fty-table make-self-table)
          (defmake-self-gen-sum-cases type (cdr prods)
                                      member-names
                                      fty-table make-self-table)))))

Theorem: true-listp-of-defmake-self-gen-sum-cases

(defthm true-listp-of-defmake-self-gen-sum-cases
  (b* ((keyword+term-list
            (defmake-self-gen-sum-cases type prods member-names
                                        fty-table make-self-table)))
    (true-listp keyword+term-list))
  :rule-classes :rewrite)