		Search-engine friendly clone of the ACL2 documentation.

Deftrans

Deftrans-defn

Signature
(deftrans-defn case names bodies args extra-args default-body extras) → *
Arguments: case — Guard (symbolp case).; names — Guard (alistp names).; bodies — Guard (alistp bodies).; args — Guard (true-listp args).; extra-args — Guard (true-listp extra-args).

Definitions and Theorems

Function: deftrans-defn

(defun deftrans-defn (case names
                       bodies
                       args extra-args default-body extras)
 (declare (xargs :guard (and (symbolp case)
                             (alistp names)
                             (alistp bodies)
                             (true-listp args)
                             (true-listp extra-args))))
 (let ((__function__ 'deftrans-defn))
  (declare (ignorable __function__))
  (b* ((lookup (assoc-eq (acl2::packn-pos (list case)
                                          (pkg-witness "KEYWORD"))
                         bodies))
       (arg-names (append (deftrans-get-args args)
                          (deftrans-get-args extra-args))))
   (cons
    'define
    (cons (cdr (assoc-eq case names))
          (cons (append args extra-args)
                (cons (cons 'declare
                            (cons (cons 'ignorable arg-names) 'nil))
                      (cons (if lookup (cons (cdr lookup) arg-names)
                              default-body)
                            extras))))))))