		Search-engine friendly clone of the ACL2 documentation.

Deftrans

Deftrans-macro

Signature
(deftrans-macro name rest) → *
Arguments: name — Guard (symbolp name).; rest — Guard (true-listp rest).

Definitions and Theorems

Function: deftrans-macro

(defun deftrans-macro (name rest)
 (declare (xargs :guard (and (symbolp name) (true-listp rest))))
 (let ((__function__ 'deftrans-macro))
  (declare (ignorable __function__))
  (b* (((mv extra-args with-output-off bodies)
        (deftrans-parse-keywords rest)))
   (cons
    'with-output
    (cons
      ':off
      (cons with-output-off
            (cons ':gag-mode
                  (cons 't
                        (cons (deftrans-core name extra-args bodies)
                              'nil)))))))))