Definition of the defmax-nat macro.
Submit the event generated by defmax-nat-fn.
Macro:
(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)))