		Search-engine friendly clone of the ACL2 documentation.

Defbyte-implementation

Defbyte-macro-definition

Definition of the defbyte macro.

Macro: defbyte

(defmacro defbyte (type &key size signed
                        pred fix equiv parents short long)
 (cons
  'make-event
  (cons
   (cons
    'defbyte-fn
    (cons
     (cons 'quote (cons type 'nil))
     (cons
      (cons 'quote (cons size 'nil))
      (cons
       (cons 'quote (cons signed 'nil))
       (cons
        (cons 'quote (cons pred 'nil))
        (cons
           (cons 'quote (cons fix 'nil))
           (cons (cons 'quote (cons equiv 'nil))
                 (cons (cons 'quote (cons parents 'nil))
                       (cons short (cons long '((w state))))))))))))
   'nil)))