		Search-engine friendly clone of the ACL2 documentation.

Deftrans

Deftrans-defn-label

Signature
(deftrans-defn-label names bodies extra-args extra-args-names) → *
Arguments: names — Guard (alistp names).; bodies — Guard (alistp bodies).; extra-args — Guard (true-listp extra-args).; extra-args-names — Guard (true-listp extra-args-names).

Definitions and Theorems

Function: deftrans-defn-label

(defun deftrans-defn-label
       (names bodies extra-args extra-args-names)
 (declare (xargs :guard (and (alistp names)
                             (alistp bodies)
                             (true-listp extra-args)
                             (true-listp extra-args-names))))
 (let ((__function__ 'deftrans-defn-label))
  (declare (ignorable __function__))
  (deftrans-defn
   'label
   names bodies '((label labelp))
   extra-args
   (cons
    'label-case
    (cons
     'label
     (cons
      ':name
      (cons
       '(label-fix label)
       (cons
        ':casexpr
        (cons
         (cons
          'make-label-casexpr
          (cons
           ':expr
           (cons
            (cons (cdr (assoc-eq 'const-expr names))
                  (cons 'label.expr extra-args-names))
            (cons
               ':range?
               (cons (cons (cdr (assoc-eq 'const-expr-option names))
                           (cons 'label.range? extra-args-names))
                     'nil)))))
         '(:default (label-fix label))))))))
   '(:returns (new-label labelp)
              :measure (label-count label)))))