Show the event form generated by defunvar, without submitting them.
Macro:
(defmacro show-defunvar (&whole call funvar arguments arrow result &key print) (cons 'defunvar-fn (cons (cons 'quote (cons funvar 'nil)) (cons (cons 'quote (cons arguments 'nil)) (cons (cons 'quote (cons arrow 'nil)) (cons (cons 'quote (cons result 'nil)) (cons (cons 'quote (cons print 'nil)) (cons (cons 'quote (cons call 'nil)) (cons (cons 'cons (cons ''defunvar (cons (cons 'quote (cons funvar 'nil)) 'nil))) '(state))))))))))
Macro:
(defmacro acl2::show-defunvar (&rest args) (cons 'show-defunvar args))