		Search-engine friendly clone of the ACL2 documentation.

Defmax-nat-implementation

Defmax-nat-macro-definition

Definition of the defmax-nat macro.

Submit the event generated by defmax-nat-fn.

Macro: defmax-nat

(defmacro defmax-nat (f y x1...xn body &key (guard 't)
                        (verify-guards 't))
 (cons
  'make-event
  (cons
   (cons
    'defmax-nat-fn
    (cons
     (cons 'quote (cons f 'nil))
     (cons
      (cons 'quote (cons y 'nil))
      (cons
       (cons 'quote (cons x1...xn 'nil))
       (cons
        (cons 'quote (cons body 'nil))
        (cons
           (cons 'quote (cons guard 'nil))
           (cons (cons 'quote (cons verify-guards 'nil))
                 (cons (cons 'cons
                             (cons ''defmax-nat
                                   (cons (cons 'quote (cons f 'nil))
                                         'nil)))
                       '(state)))))))))
   'nil)))