		Search-engine friendly clone of the ACL2 documentation.

Deffixer-implementation

Deffixer-macro-definition

Definition of the deffixer macro.

Macro: deffixer

(defmacro deffixer (name &key pred param body-fix
                         (parents 'nil parents-supplied-p)
                         (short 'nil short-supplied-p)
                         (long 'nil long-supplied-p))
 (cons
  'make-event
  (cons
   (cons
    'deffixer-fn
    (cons
     (cons 'quote (cons name 'nil))
     (cons
      (cons 'quote (cons pred 'nil))
      (cons
       (cons 'quote (cons param 'nil))
       (cons
        (cons 'quote (cons body-fix 'nil))
        (cons
         (cons 'quote (cons parents 'nil))
         (cons
             parents-supplied-p
             (cons short
                   (cons short-supplied-p
                         (cons long
                               (cons long-supplied-p 'nil)))))))))))
   'nil)))