		Search-engine friendly clone of the ACL2 documentation.

Defun-inst-implementation

Show-defun-inst

Show the event form generated by defun-inst, without submitting them.

Macro: show-defun-inst

(defmacro show-defun-inst (fun sofun-inst &rest rest)
 (cons
  'defun-inst-fn
  (cons
   (cons 'quote (cons fun 'nil))
   (cons (cons 'quote (cons sofun-inst 'nil))
         (cons (cons 'quote (cons rest 'nil))
               (cons (cons 'cons
                           (cons ''defun-inst
                                 (cons (cons 'quote (cons fun 'nil))
                                       'nil)))
                     '(state)))))))

Macro: show-defun-inst

(defmacro acl2::show-defun-inst (&rest args)
  (cons 'show-defun-inst args))