		Search-engine friendly clone of the ACL2 documentation.

Defbytelist-standard-instances

Defubytelist

Specialized form of defbytelist for generating standard fixtypes of true lists of unsigned bytes of explicit integer sizes.

This macro just takes a positive integer as input.

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

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

Macro: defubytelist

(defmacro defubytelist (size)
 (declare (xargs :guard (posp size)))
 (cons
  'defbytelist
  (cons
   (acl2::packn (list 'acl2::ubyte size '-list))
   (cons
    ':elt-type
    (cons
     (acl2::packn (list 'acl2::ubyte size))
     (cons
      ':pred
      (cons
       (acl2::packn (list 'acl2::ubyte size '-listp))
       (cons
        ':fix
        (cons
         (acl2::packn (list 'acl2::ubyte size '-list-fix))
         (cons
          ':equiv
          (cons
           (acl2::packn (list 'acl2::ubyte size '-list-equiv))
           (cons
            ':parents
            (cons
             '(defbytelist-standard-instances)
             (cons
              ':short
              (cons
               (concatenate
                  'string
                  "Fixtype of true lists of unsigned bytes of size "
                  (coerce (explode-nonnegative-integer size 10 nil)
                          'string)
                  ".")
               'nil)))))))))))))))