		Search-engine friendly clone of the ACL2 documentation.

Defunvar-implementation

Defunvar-macro-definition

Definition of the defunvar macro.

Macro: defunvar

(defmacro defunvar (&whole call &rest inputs)
 (cons
  'make-event-terse
  (cons
   (cons
    'defunvar-fn
    (cons
     (cons 'quote (cons inputs 'nil))
     (cons
      (cons 'quote (cons call 'nil))
      (cons
       (cons
        'cons
        (cons ''defunvar
              (cons (cons 'quote
                          (cons (if (consp inputs) (car inputs) nil)
                                'nil))
                    'nil)))
       '(state)))))
   'nil)))

Macro: defunvar

(defmacro acl2::defunvar (&rest inputs)
  (cons 'defunvar inputs))