		Search-engine friendly clone of the ACL2 documentation.
Def-error-checker-implementation
Def-error-checker-macro-definition

Definition of the def-error-checker macro.
Macro: def-error-checker
(defmacro def-error-checker
          (&whole def-error-checker-call name xs &key
                  body (returns 'nil returns-supplied-p)
                  (result 'nil)
                  (mode ':logic)
                  (verify-guards 'nil
                                 verify-guards-supplied-p)
                  (parents 'nil parents-supplied-p)
                  (short '"" short-supplied-p)
                  (long '"" long-supplied-p))
 (cons
  'make-event
  (cons
   (cons
    'def-error-checker-fn
    (cons
     (cons 'quote (cons name 'nil))
     (cons
      (cons 'quote (cons xs 'nil))
      (cons
       (cons 'quote (cons returns 'nil))
       (cons
        (cons 'quote
              (cons returns-supplied-p 'nil))
        (cons
         (cons 'quote (cons body 'nil))
         (cons
          (cons 'quote (cons result 'nil))
          (cons
           (cons 'quote (cons mode 'nil))
           (cons
            (cons 'quote (cons verify-guards 'nil))
            (cons
             (cons 'quote
                   (cons verify-guards-supplied-p 'nil))
             (cons
              (cons 'quote (cons parents 'nil))
              (cons
               (cons 'quote
                     (cons parents-supplied-p 'nil))
               (cons
                (cons 'quote (cons short 'nil))
                (cons
                 (cons 'quote
                       (cons short-supplied-p 'nil))
                 (cons
                  (cons 'quote (cons long 'nil))
                  (cons
                     (cons 'quote
                           (cons long-supplied-p 'nil))
                     (cons (cons 'quote
                                 (cons def-error-checker-call 'nil))
                           '(state))))))))))))))))))
   'nil)))