		Search-engine friendly clone of the ACL2 documentation.

Atj-implementation

Atj-macro-definition

Definition of the atj macro.

We suppress the extra output produced by make-event via with-output and (:on-behalf-of :quiet).

Macro: atj

(defmacro atj (&rest args)
 (cons
  'with-output
  (cons
   ':off
   (cons
    ':all
    (cons
     ':on
     (cons
        'error
        (cons (cons 'make-event
                    (cons (cons 'atj-fn
                                (cons (cons 'quote (cons args 'nil))
                                      '('atj state)))
                          '(:on-behalf-of :quiet)))
              'nil)))))))