		Search-engine friendly clone of the ACL2 documentation.

Deftrans

Deftrans-defn-const-expr

Signature
(deftrans-defn-const-expr 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-const-expr

(defun deftrans-defn-const-expr
       (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-const-expr))
    (declare (ignorable __function__))
    (deftrans-defn 'const-expr
                   names bodies '((cexpr const-exprp))
                   extra-args
                   (cons 'const-expr
                         (cons (cons (cdr (assoc-eq 'expr names))
                                     (cons '(const-expr->expr cexpr)
                                           extra-args-names))
                               'nil))
                   '(:returns (new-cexpr const-exprp)
                              :measure (const-expr-count cexpr)))))