		Search-engine friendly clone of the ACL2 documentation.

Defunvar-implementation

Show-defunvar

Show the event form generated by defunvar, without submitting them.

Macro: show-defunvar

(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: show-defunvar

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