		Search-engine friendly clone of the ACL2 documentation.

Defbyte-standard-instances

Defubyte

Specialized form of defbyte for generating standard fixtypes of unsigned bytes of explicit integer sizes.

This macro just takes a positive integer as input.

This macro generates fixtypes called acl2::ubyte<size>, where <size> consists of the decimal digits of the size. The recognizer, fixer, and equivalence are called acl2::ubyte<size>p, acl2::ubyte<size>-fix, and acl2::ubyte<size>-equiv.

This macro also generates some standardized XDOC parents and short, and no XDOC long.

Macro: defubyte

(defmacro defubyte (size)
 (declare (xargs :guard (posp size)))
 (cons
  'defbyte
  (cons
   (acl2::packn (list 'acl2::ubyte size))
   (cons
    ':size
    (cons
     size
     (cons
      ':signed
      (cons
       'nil
       (cons
        ':pred
        (cons
         (acl2::packn (list 'acl2::ubyte size 'p))
         (cons
          ':fix
          (cons
           (acl2::packn (list 'acl2::ubyte size '-fix))
           (cons
            ':equiv
            (cons
             (acl2::packn (list 'acl2::ubyte size '-equiv))
             (cons
              ':parents
              (cons
               '(defbyte-standard-instances)
               (cons
                ':short
                (cons
                 (concatenate
                   'string
                   "Fixtype of unsigned bytes of size "
                   (coerce (explode-nonnegative-integer size 10 nil)
                           'string)
                   ".")
                 'nil)))))))))))))))))