		Search-engine friendly clone of the ACL2 documentation.

Deftrans

Deftrans-mk-names0

Signature
(deftrans-mk-names0 name cases) → names
Arguments: name — Guard (symbolp name).; cases — Guard (symbol-listp cases).
Returns: names — Type (symbol-alistp names).

Definitions and Theorems

Function: deftrans-mk-names0

(defun deftrans-mk-names0 (name cases)
  (declare (xargs :guard (and (symbolp name)
                              (symbol-listp cases))))
  (let ((__function__ 'deftrans-mk-names0))
    (declare (ignorable __function__))
    (if (endp cases)
        nil
      (cons (cons (mbe :logic (and (symbolp (first cases))
                                   (first cases))
                       :exec (first cases))
                  (packn-pos (list name '- (first cases))
                             name))
            (deftrans-mk-names0 name (rest cases))))))

Theorem: symbol-alistp-of-deftrans-mk-names0

(defthm symbol-alistp-of-deftrans-mk-names0
  (b* ((names (deftrans-mk-names0 name cases)))
    (symbol-alistp names))
  :rule-classes :rewrite)